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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4d  203  ifnebibdc  3686  ssprsseq  3877  nlimsucg  4715  ssrelrn  4974  poltletr  5191  xp11m  5229  fvmptdf  5796  elfvmptrab1  5804  eusvobj2  6074  ovmpodf  6223  elovmporab  6292  elovmporab1w  6293  f1o2ndf1  6468  suppssdc  6504  suppssrst  6505  suppssrgst  6506  smoiso  6578  nnsseleq  6779  ecopovtrn  6911  ecopovtrng  6914  dom2lem  7064  fundmen  7100  dom1o  7122  fidifsnen  7178  findcard2  7199  findcard2s  7200  supisoex  7355  infglbti  7371  ordiso2  7381  updjud  7428  difinfsnlem  7445  enomnilem  7484  enmkvlem  7507  netap  7626  2omotaplemap  7629  cc2lem  7638  addcanpig  7707  mulcanpig  7708  addnidpig  7709  ordpipqqs  7747  ltexnqq  7781  prarloclemlo  7867  genpcdl  7892  genpcuu  7893  mulnqprl  7941  mulnqpru  7942  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  distrlem5prl  7959  distrlem5pru  7960  ltsopr  7969  ltexprlemfl  7982  ltexprlemfu  7984  recexprlemss1l  8008  recexprlemss1u  8009  aptiprleml  8012  ltsrprg  8120  lttrsr  8135  mulextsr1lem  8153  axapti  8402  cnegexlem1  8508  le2add  8779  lt2add  8780  ltleadd  8781  lt2sub  8795  le2sub  8796  recexre  8914  reapti  8915  apreap  8923  reapcotr  8934  remulext1  8935  apreim  8939  apcotr  8943  mulext2  8949  recexap  8989  addltmul  9553  elnnz  9663  zleloe  9700  difgtsumgt  9723  nn0n0n1ge2b  9734  nn0lt2  9736  nn0le2is012  9737  zextlt  9748  uzind2  9768  supinfneg  10010  infsupneg  10011  eluzdc  10025  qreccl  10057  elpq  10065  xltnegi  10253  xnn0lenn0nn0  10283  iccid  10343  icoshft  10408  zltaddlt1le  10426  fzofzim  10616  qbtwnxr  10708  flqeqceilz  10775  modqmuladdnn0  10825  modfzo0difsn  10852  addmodlteq  10855  frec2uzrand  10862  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  seqf1oglem1  10976  facdiv  11197  facwordi  11199  faclbnd  11200  bcpasc  11225  seq3coll  11315  fundm2domnop0  11321  fstwrdne  11364  elovmpowrd  11367  lswlgt0cl  11378  ccatrn  11398  ccatalpha  11402  swrdnd  11452  swrdswrd  11498  wrd2ind  11516  swrdccatin1  11518  pfxccatin12lem2a  11520  pfxccat3  11527  swrdccat  11528  swrdccat3blem  11532  reuccatpfxs1lem  11539  recvguniq  11782  abs00ap  11849  absext  11850  absnid  11860  cau3lem  11902  climuni  12083  2clim  12091  summodc  12174  fisumss  12183  fsumabs  12256  mertenslem2  12327  fprodssdc  12381  reeff1  12491  efieq1re  12563  dvdsmultr2  12624  dvdsleabs  12636  odd2np1lem  12663  odd2np1  12664  ltoddhalfle  12684  halfleoddlt  12685  m1expo  12691  nn0enne  12693  nn0ehalf  12694  nn0o1gt2  12696  flodddiv4  12727  zeqzmulgcd  12771  gcdneg  12783  gcdaddm  12785  bezoutlemaz  12804  bezoutlembz  12805  dfgcd2  12815  gcddiv  12820  dvdssqim  12825  algcvgblem  12851  algcvga  12853  lcmneg  12876  coprmgcdb  12890  coprmdvds2  12895  qredeq  12898  divgcdcoprm0  12903  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  prmind2  12922  dvdsnprmd  12927  prmgt1  12935  nprmdvds1  12943  divgcdodd  12946  euclemma  12949  prmdvdsexpr  12953  prmfac1  12955  prmndvdsfaclt  12959  crth  13030  eulerthlemh  13037  fermltl  13040  nnnn0modprm0  13062  coprimeprodsq2  13065  pythagtriplem2  13073  pcpremul  13100  pcdvdsb  13127  pc2dvds  13137  pc11  13138  dvdsprmpweqnn  13143  dvdsprmpweqle  13144  difsqpwdvds  13145  pcfac  13157  oddprmdvds  13161  prmpwdvds  13162  1arith  13174  4sqlem11  13208  4sqlem12  13209  prmlem0  13248  ballotfilemfrceq  13329  imasaddfnlemg  13693  erlecpbl  13711  xpsff1o  13728  imasmnd2  13817  grp1inv  13970  imasgrp2  13971  ghmpreima  14127  imasabl  14229  imasrng  14361  imasring  14477  dvdsrtr  14516  dvdsrmul1  14517  unitgrp  14531  znidomb  15101  tgtop  15311  tgidm  15317  neipsm  15397  restbasg  15411  tgrest  15412  tgcn  15451  tgcnp  15452  cnconst2  15476  cnconst  15477  cnptopresti  15481  txbasval  15510  txcnp  15514  txdis1cn  15521  bldisj  15644  xblm  15660  blssps  15670  blss  15671  blin2  15675  cnlimcim  15914  dveflem  15969  sincosq3sgn  16072  sincosq4sgn  16073  coseq0q4123  16078  sineq0re  16093  ioocosf1o  16099  logbgcd1irr  16220  birthdaylem1g  16242  pellexlem1  16246  pellexlem3  16248  mpodvdsmulf1o  16301  ppiublem1  16308  chtqub  16313  bclbnd  16324  bposlem1  16328  bposlem5  16332  zabsle1  16340  lgsdir2lem5  16373  lgsne0  16379  lgsdirnn0  16388  gausslemma2dlem0i  16398  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  gausslemma2dlem7  16409  gausslemma2d  16410  lgseisenlem2  16412  lgsquadlem1  16418  2lgslem1a1  16427  2lgslem1b  16430  2lgslem1c  16431  2lgs  16445  2lgsoddprmlem2  16447  upgrpredgv  16609  ausgrumgrien  16633  ausgrusgrien  16634  usgruspgrben  16649  uhgr2edg  16669  usgredg4  16678  ushgredgedg  16689  ushgredgedgloop  16691  edg0usgr  16710  uhgrspansubgrlem  16739  wlkl1loop  16821  wlk1walkdom  16822  wlklenvclwlk  16836  wlkres  16842  clwwlknonex2  16902  uzdcinzz  17048  subctctexmid  17252