Theorem sylbid 148

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
sylbid.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylbid	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylbid

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 142	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbid.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 44	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr4d  201  nlimsucg  4309  poltletr  4745  xp11m  4779  fvmptdf  5279  eusvobj2  5518  ovmpt2df  5652  f1o2ndf1  5869  smoiso  5940  nnsseleq  6102  ecopovtrn  6226  ecopovtrng  6229  dom2lem  6275  fundmen  6309  fidifsnen  6355  findcard2  6373  findcard2s  6374  supisoex  6422  infglbti  6438  ordiso2  6446  addcanpig  6524  mulcanpig  6525  addnidpig  6526  ordpipqqs  6564  ltexnqq  6598  prarloclemlo  6684  genpcdl  6709  genpcuu  6710  mulnqprl  6758  mulnqpru  6759  distrlem1prl  6772  distrlem1pru  6773  distrlem4prl  6774  distrlem4pru  6775  distrlem5prl  6776  distrlem5pru  6777  ltsopr  6786  ltexprlemfl  6799  ltexprlemfu  6801  recexprlemss1l  6825  recexprlemss1u  6826  aptiprleml  6829  ltsrprg  6924  lttrsr  6939  mulextsr1lem  6956  axapti  7183  cnegexlem1  7283  le2add  7548  lt2add  7549  ltleadd  7550  lt2sub  7564  le2sub  7565  recexre  7678  reapti  7679  apreap  7687  reapcotr  7698  remulext1  7699  apreim  7703  apcotr  7707  mulext2  7713  recexap  7743  addltmul  8267  elnnz  8361  zleloe  8398  nn0n0n1ge2b  8427  nn0lt2  8429  zextlt  8439  uzind2  8459  supinfneg  8683  infsupneg  8684  eluzdc  8697  qreccl  8727  xltnegi  8902  iccid  8948  icoshft  9012  zltaddlt1le  9028  fzofzim  9197  qbtwnxr  9266  flqeqceilz  9320  modqmuladdnn0  9370  modfzo0difsn  9397  addmodlteq  9400  frec2uzrand  9407  frecuzrdgfn  9414  facdiv  9665  facwordi  9667  faclbnd  9668  bcpasc  9693  recvguniq  9881  abs00ap  9948  absext  9949  absnid  9959  cau3lem  10000  climuni  10132  2clim  10140  dvdsmultr2  10235  dvdsleabs  10245  odd2np1lem  10271  odd2np1  10272  ltoddhalfle  10293  halfleoddlt  10294  m1expo  10300  nn0enne  10302  nn0ehalf  10303  nn0o1gt2  10305  flodddiv4  10334  zeqzmulgcd  10362  gcdneg  10373  gcdaddm  10375  bezoutlemaz  10392  bezoutlembz  10393  dfgcd2  10403  gcddiv  10408  dvdssqim  10413  algcvgblem  10431  ialgcvga  10433  lcmneg  10456  coprmgcdb  10470  coprmdvds2  10475  qredeq  10478  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  prmind2  10502  dvdsnprmd  10507  prmgt1  10513  nprmdvds1  10521  divgcdodd  10522  euclemma  10525  prmdvdsexpr  10529  prmfac1  10531  prmndvdsfaclt  10535