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  nlimsucg  4565  poltletr  5029  xp11m  5067  fvmptdf  5603  elfvmptrab1  5610  eusvobj2  5860  ovmpodf  6005  f1o2ndf1  6228  smoiso  6302  nnsseleq  6501  ecopovtrn  6631  ecopovtrng  6634  dom2lem  6771  fundmen  6805  fidifsnen  6869  findcard2  6888  findcard2s  6889  supisoex  7007  infglbti  7023  ordiso2  7033  updjud  7080  difinfsnlem  7097  enomnilem  7135  enmkvlem  7158  netap  7252  2omotaplemap  7255  cc2lem  7264  addcanpig  7332  mulcanpig  7333  addnidpig  7334  ordpipqqs  7372  ltexnqq  7406  prarloclemlo  7492  genpcdl  7517  genpcuu  7518  mulnqprl  7566  mulnqpru  7567  distrlem1prl  7580  distrlem1pru  7581  distrlem4prl  7582  distrlem4pru  7583  distrlem5prl  7584  distrlem5pru  7585  ltsopr  7594  ltexprlemfl  7607  ltexprlemfu  7609  recexprlemss1l  7633  recexprlemss1u  7634  aptiprleml  7637  ltsrprg  7745  lttrsr  7760  mulextsr1lem  7778  axapti  8027  cnegexlem1  8131  le2add  8400  lt2add  8401  ltleadd  8402  lt2sub  8416  le2sub  8417  recexre  8534  reapti  8535  apreap  8543  reapcotr  8554  remulext1  8555  apreim  8559  apcotr  8563  mulext2  8569  recexap  8609  addltmul  9154  elnnz  9262  zleloe  9299  difgtsumgt  9321  nn0n0n1ge2b  9331  nn0lt2  9333  nn0le2is012  9334  zextlt  9344  uzind2  9364  supinfneg  9594  infsupneg  9595  eluzdc  9609  qreccl  9641  elpq  9647  xltnegi  9834  xnn0lenn0nn0  9864  iccid  9924  icoshft  9989  zltaddlt1le  10006  fzofzim  10187  qbtwnxr  10257  flqeqceilz  10317  modqmuladdnn0  10367  modfzo0difsn  10394  addmodlteq  10397  frec2uzrand  10404  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  facdiv  10717  facwordi  10719  faclbnd  10720  bcpasc  10745  seq3coll  10821  recvguniq  11003  abs00ap  11070  absext  11071  absnid  11081  cau3lem  11122  climuni  11300  2clim  11308  summodc  11390  fisumss  11399  fsumabs  11472  mertenslem2  11543  fprodssdc  11597  reeff1  11707  efieq1re  11778  dvdsmultr2  11839  dvdsleabs  11850  odd2np1lem  11876  odd2np1  11877  ltoddhalfle  11897  halfleoddlt  11898  m1expo  11904  nn0enne  11906  nn0ehalf  11907  nn0o1gt2  11909  flodddiv4  11938  zeqzmulgcd  11970  gcdneg  11982  gcdaddm  11984  bezoutlemaz  12003  bezoutlembz  12004  dfgcd2  12014  gcddiv  12019  dvdssqim  12024  algcvgblem  12048  algcvga  12050  lcmneg  12073  coprmgcdb  12087  coprmdvds2  12092  qredeq  12095  divgcdcoprm0  12100  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  prmind2  12119  dvdsnprmd  12124  prmgt1  12131  nprmdvds1  12139  divgcdodd  12142  euclemma  12145  prmdvdsexpr  12149  prmfac1  12151  prmndvdsfaclt  12155  crth  12223  eulerthlemh  12230  fermltl  12233  nnnn0modprm0  12254  coprimeprodsq2  12257  pythagtriplem2  12265  pcpremul  12292  pcdvdsb  12318  pc2dvds  12328  pc11  12329  dvdsprmpweqnn  12334  dvdsprmpweqle  12335  difsqpwdvds  12336  pcfac  12347  oddprmdvds  12351  prmpwdvds  12352  1arith  12364  imasaddfnlemg  12734  erlecpbl  12750  xpsff1o  12767  grp1inv  12976  dvdsrtr  13268  dvdsrmul1  13269  unitgrp  13283  tgtop  13538  tgidm  13544  neipsm  13624  restbasg  13638  tgrest  13639  tgcn  13678  tgcnp  13679  cnconst2  13703  cnconst  13704  cnptopresti  13708  txbasval  13737  txcnp  13741  txdis1cn  13748  bldisj  13871  xblm  13887  blssps  13897  blss  13898  blin2  13902  cnlimcim  14110  dveflem  14157  sincosq3sgn  14219  sincosq4sgn  14220  coseq0q4123  14225  ioocosf1o  14245  logbgcd1irr  14355  zabsle1  14370  lgsdir2lem5  14403  lgsne0  14409  lgsdirnn0  14418  lgseisenlem2  14421  2lgsoddprmlem2  14424  uzdcinzz  14520  subctctexmid  14720