Theorem sylbid 150

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 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbid.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr4d  203  ifnebibdc  3651  ssprsseq  3835  nlimsucg  4664  ssrelrn  4922  poltletr  5137  xp11m  5175  fvmptdf  5734  elfvmptrab1  5741  eusvobj2  6003  ovmpodf  6152  elovmporab  6221  elovmporab1w  6222  f1o2ndf1  6392  smoiso  6467  nnsseleq  6668  ecopovtrn  6800  ecopovtrng  6803  dom2lem  6944  fundmen  6980  dom1o  7001  fidifsnen  7056  findcard2  7077  findcard2s  7078  supisoex  7207  infglbti  7223  ordiso2  7233  updjud  7280  difinfsnlem  7297  enomnilem  7336  enmkvlem  7359  netap  7472  2omotaplemap  7475  cc2lem  7484  addcanpig  7553  mulcanpig  7554  addnidpig  7555  ordpipqqs  7593  ltexnqq  7627  prarloclemlo  7713  genpcdl  7738  genpcuu  7739  mulnqprl  7787  mulnqpru  7788  distrlem1prl  7801  distrlem1pru  7802  distrlem4prl  7803  distrlem4pru  7804  distrlem5prl  7805  distrlem5pru  7806  ltsopr  7815  ltexprlemfl  7828  ltexprlemfu  7830  recexprlemss1l  7854  recexprlemss1u  7855  aptiprleml  7858  ltsrprg  7966  lttrsr  7981  mulextsr1lem  7999  axapti  8249  cnegexlem1  8353  le2add  8623  lt2add  8624  ltleadd  8625  lt2sub  8639  le2sub  8640  recexre  8757  reapti  8758  apreap  8766  reapcotr  8777  remulext1  8778  apreim  8782  apcotr  8786  mulext2  8792  recexap  8832  addltmul  9380  elnnz  9488  zleloe  9525  difgtsumgt  9548  nn0n0n1ge2b  9558  nn0lt2  9560  nn0le2is012  9561  zextlt  9571  uzind2  9591  supinfneg  9828  infsupneg  9829  eluzdc  9843  qreccl  9875  elpq  9882  xltnegi  10069  xnn0lenn0nn0  10099  iccid  10159  icoshft  10224  zltaddlt1le  10241  fzofzim  10426  qbtwnxr  10516  flqeqceilz  10579  modqmuladdnn0  10629  modfzo0difsn  10656  addmodlteq  10659  frec2uzrand  10666  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  seqf1oglem1  10780  facdiv  10999  facwordi  11001  faclbnd  11002  bcpasc  11027  seq3coll  11105  fundm2domnop0  11108  fstwrdne  11151  elovmpowrd  11154  lswlgt0cl  11165  ccatrn  11185  ccatalpha  11189  swrdnd  11239  swrdswrd  11285  wrd2ind  11303  swrdccatin1  11305  pfxccatin12lem2a  11307  pfxccat3  11314  swrdccat  11315  swrdccat3blem  11319  reuccatpfxs1lem  11326  recvguniq  11555  abs00ap  11622  absext  11623  absnid  11633  cau3lem  11674  climuni  11853  2clim  11861  summodc  11943  fisumss  11952  fsumabs  12025  mertenslem2  12096  fprodssdc  12150  reeff1  12260  efieq1re  12332  dvdsmultr2  12393  dvdsleabs  12405  odd2np1lem  12432  odd2np1  12433  ltoddhalfle  12453  halfleoddlt  12454  m1expo  12460  nn0enne  12462  nn0ehalf  12463  nn0o1gt2  12465  flodddiv4  12496  zeqzmulgcd  12540  gcdneg  12552  gcdaddm  12554  bezoutlemaz  12573  bezoutlembz  12574  dfgcd2  12584  gcddiv  12589  dvdssqim  12594  algcvgblem  12620  algcvga  12622  lcmneg  12645  coprmgcdb  12659  coprmdvds2  12664  qredeq  12667  divgcdcoprm0  12672  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  prmind2  12691  dvdsnprmd  12696  prmgt1  12703  nprmdvds1  12711  divgcdodd  12714  euclemma  12717  prmdvdsexpr  12721  prmfac1  12723  prmndvdsfaclt  12727  crth  12795  eulerthlemh  12802  fermltl  12805  nnnn0modprm0  12827  coprimeprodsq2  12830  pythagtriplem2  12838  pcpremul  12865  pcdvdsb  12892  pc2dvds  12902  pc11  12903  dvdsprmpweqnn  12908  dvdsprmpweqle  12909  difsqpwdvds  12910  pcfac  12922  oddprmdvds  12926  prmpwdvds  12927  1arith  12939  4sqlem11  12973  4sqlem12  12974  imasaddfnlemg  13396  erlecpbl  13414  xpsff1o  13431  imasmnd2  13534  grp1inv  13689  imasgrp2  13696  ghmpreima  13852  imasabl  13922  imasrng  13968  imasring  14076  dvdsrtr  14114  dvdsrmul1  14115  unitgrp  14129  znidomb  14671  tgtop  14791  tgidm  14797  neipsm  14877  restbasg  14891  tgrest  14892  tgcn  14931  tgcnp  14932  cnconst2  14956  cnconst  14957  cnptopresti  14961  txbasval  14990  txcnp  14994  txdis1cn  15001  bldisj  15124  xblm  15140  blssps  15150  blss  15151  blin2  15155  cnlimcim  15394  dveflem  15449  sincosq3sgn  15551  sincosq4sgn  15552  coseq0q4123  15557  ioocosf1o  15577  logbgcd1irr  15690  mpodvdsmulf1o  15713  zabsle1  15727  lgsdir2lem5  15760  lgsne0  15766  lgsdirnn0  15775  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  gausslemma2dlem7  15796  gausslemma2d  15797  lgseisenlem2  15799  lgsquadlem1  15805  2lgslem1a1  15814  2lgslem1b  15817  2lgslem1c  15818  2lgs  15832  2lgsoddprmlem2  15834  upgrpredgv  15996  ausgrumgrien  16020  ausgrusgrien  16021  usgruspgrben  16036  uhgr2edg  16056  usgredg4  16065  ushgredgedg  16076  ushgredgedgloop  16078  edg0usgr  16097  uhgrspansubgrlem  16126  wlkl1loop  16208  wlk1walkdom  16209  wlklenvclwlk  16223  wlkres  16229  clwwlknonex2  16289  uzdcinzz  16394  subctctexmid  16601