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  3683  ssprsseq  3872  nlimsucg  4708  ssrelrn  4967  poltletr  5183  xp11m  5221  fvmptdf  5787  elfvmptrab1  5794  eusvobj2  6061  ovmpodf  6210  elovmporab  6279  elovmporab1w  6280  f1o2ndf1  6454  suppssdc  6490  suppssrst  6491  suppssrgst  6492  smoiso  6563  nnsseleq  6764  ecopovtrn  6896  ecopovtrng  6899  dom2lem  7048  fundmen  7084  dom1o  7106  fidifsnen  7162  findcard2  7183  findcard2s  7184  supisoex  7339  infglbti  7355  ordiso2  7365  updjud  7412  difinfsnlem  7429  enomnilem  7468  enmkvlem  7491  netap  7610  2omotaplemap  7613  cc2lem  7622  addcanpig  7691  mulcanpig  7692  addnidpig  7693  ordpipqqs  7731  ltexnqq  7765  prarloclemlo  7851  genpcdl  7876  genpcuu  7877  mulnqprl  7925  mulnqpru  7926  distrlem1prl  7939  distrlem1pru  7940  distrlem4prl  7941  distrlem4pru  7942  distrlem5prl  7943  distrlem5pru  7944  ltsopr  7953  ltexprlemfl  7966  ltexprlemfu  7968  recexprlemss1l  7992  recexprlemss1u  7993  aptiprleml  7996  ltsrprg  8104  lttrsr  8119  mulextsr1lem  8137  axapti  8386  cnegexlem1  8491  le2add  8762  lt2add  8763  ltleadd  8764  lt2sub  8778  le2sub  8779  recexre  8896  reapti  8897  apreap  8905  reapcotr  8916  remulext1  8917  apreim  8921  apcotr  8925  mulext2  8931  recexap  8971  addltmul  9521  elnnz  9633  zleloe  9670  difgtsumgt  9693  nn0n0n1ge2b  9704  nn0lt2  9706  nn0le2is012  9707  zextlt  9717  uzind2  9737  supinfneg  9974  infsupneg  9975  eluzdc  9989  qreccl  10021  elpq  10028  xltnegi  10216  xnn0lenn0nn0  10246  iccid  10306  icoshft  10371  zltaddlt1le  10389  fzofzim  10578  qbtwnxr  10670  flqeqceilz  10733  modqmuladdnn0  10783  modfzo0difsn  10810  addmodlteq  10813  frec2uzrand  10820  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  seqf1oglem1  10934  facdiv  11154  facwordi  11156  faclbnd  11157  bcpasc  11182  seq3coll  11272  fundm2domnop0  11278  fstwrdne  11321  elovmpowrd  11324  lswlgt0cl  11335  ccatrn  11355  ccatalpha  11359  swrdnd  11409  swrdswrd  11455  wrd2ind  11473  swrdccatin1  11475  pfxccatin12lem2a  11477  pfxccat3  11484  swrdccat  11485  swrdccat3blem  11489  reuccatpfxs1lem  11496  recvguniq  11739  abs00ap  11806  absext  11807  absnid  11817  cau3lem  11858  climuni  12037  2clim  12045  summodc  12128  fisumss  12137  fsumabs  12210  mertenslem2  12281  fprodssdc  12335  reeff1  12445  efieq1re  12517  dvdsmultr2  12578  dvdsleabs  12590  odd2np1lem  12617  odd2np1  12618  ltoddhalfle  12638  halfleoddlt  12639  m1expo  12645  nn0enne  12647  nn0ehalf  12648  nn0o1gt2  12650  flodddiv4  12681  zeqzmulgcd  12725  gcdneg  12737  gcdaddm  12739  bezoutlemaz  12758  bezoutlembz  12759  dfgcd2  12769  gcddiv  12774  dvdssqim  12779  algcvgblem  12805  algcvga  12807  lcmneg  12830  coprmgcdb  12844  coprmdvds2  12849  qredeq  12852  divgcdcoprm0  12857  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  prmind2  12876  dvdsnprmd  12881  prmgt1  12888  nprmdvds1  12896  divgcdodd  12899  euclemma  12902  prmdvdsexpr  12906  prmfac1  12908  prmndvdsfaclt  12912  crth  12980  eulerthlemh  12987  fermltl  12990  nnnn0modprm0  13012  coprimeprodsq2  13015  pythagtriplem2  13023  pcpremul  13050  pcdvdsb  13077  pc2dvds  13087  pc11  13088  dvdsprmpweqnn  13093  dvdsprmpweqle  13094  difsqpwdvds  13095  pcfac  13107  oddprmdvds  13111  prmpwdvds  13112  1arith  13124  4sqlem11  13158  4sqlem12  13159  ballotfilemfrceq  13250  imasaddfnlemg  13612  erlecpbl  13630  xpsff1o  13647  imasmnd2  13736  grp1inv  13889  imasgrp2  13890  ghmpreima  14046  imasabl  14117  imasrng  14230  imasring  14342  dvdsrtr  14381  dvdsrmul1  14382  unitgrp  14396  znidomb  14965  tgtop  15092  tgidm  15098  neipsm  15178  restbasg  15192  tgrest  15193  tgcn  15232  tgcnp  15233  cnconst2  15257  cnconst  15258  cnptopresti  15262  txbasval  15291  txcnp  15295  txdis1cn  15302  bldisj  15425  xblm  15441  blssps  15451  blss  15452  blin2  15456  cnlimcim  15695  dveflem  15750  sincosq3sgn  15852  sincosq4sgn  15853  coseq0q4123  15858  ioocosf1o  15878  logbgcd1irr  15992  pellexlem1  16005  pellexlem3  16007  mpodvdsmulf1o  16018  zabsle1  16032  lgsdir2lem5  16065  lgsne0  16071  lgsdirnn0  16080  gausslemma2dlem0i  16090  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  gausslemma2dlem7  16101  gausslemma2d  16102  lgseisenlem2  16104  lgsquadlem1  16110  2lgslem1a1  16119  2lgslem1b  16122  2lgslem1c  16123  2lgs  16137  2lgsoddprmlem2  16139  upgrpredgv  16301  ausgrumgrien  16325  ausgrusgrien  16326  usgruspgrben  16341  uhgr2edg  16361  usgredg4  16370  ushgredgedg  16381  ushgredgedgloop  16383  edg0usgr  16402  uhgrspansubgrlem  16431  wlkl1loop  16513  wlk1walkdom  16514  wlklenvclwlk  16528  wlkres  16534  clwwlknonex2  16594  uzdcinzz  16740  subctctexmid  16944