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  3615  nlimsucg  4614  poltletr  5083  xp11m  5121  fvmptdf  5667  elfvmptrab1  5674  eusvobj2  5930  ovmpodf  6077  elovmporab  6146  elovmporab1w  6147  f1o2ndf1  6314  smoiso  6388  nnsseleq  6587  ecopovtrn  6719  ecopovtrng  6722  dom2lem  6863  fundmen  6898  fidifsnen  6967  findcard2  6986  findcard2s  6987  supisoex  7111  infglbti  7127  ordiso2  7137  updjud  7184  difinfsnlem  7201  enomnilem  7240  enmkvlem  7263  netap  7366  2omotaplemap  7369  cc2lem  7378  addcanpig  7447  mulcanpig  7448  addnidpig  7449  ordpipqqs  7487  ltexnqq  7521  prarloclemlo  7607  genpcdl  7632  genpcuu  7633  mulnqprl  7681  mulnqpru  7682  distrlem1prl  7695  distrlem1pru  7696  distrlem4prl  7697  distrlem4pru  7698  distrlem5prl  7699  distrlem5pru  7700  ltsopr  7709  ltexprlemfl  7722  ltexprlemfu  7724  recexprlemss1l  7748  recexprlemss1u  7749  aptiprleml  7752  ltsrprg  7860  lttrsr  7875  mulextsr1lem  7893  axapti  8143  cnegexlem1  8247  le2add  8517  lt2add  8518  ltleadd  8519  lt2sub  8533  le2sub  8534  recexre  8651  reapti  8652  apreap  8660  reapcotr  8671  remulext1  8672  apreim  8676  apcotr  8680  mulext2  8686  recexap  8726  addltmul  9274  elnnz  9382  zleloe  9419  difgtsumgt  9442  nn0n0n1ge2b  9452  nn0lt2  9454  nn0le2is012  9455  zextlt  9465  uzind2  9485  supinfneg  9716  infsupneg  9717  eluzdc  9731  qreccl  9763  elpq  9770  xltnegi  9957  xnn0lenn0nn0  9987  iccid  10047  icoshft  10112  zltaddlt1le  10129  fzofzim  10312  qbtwnxr  10400  flqeqceilz  10463  modqmuladdnn0  10513  modfzo0difsn  10540  addmodlteq  10543  frec2uzrand  10550  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  seqf1oglem1  10664  facdiv  10883  facwordi  10885  faclbnd  10886  bcpasc  10911  seq3coll  10987  fundm2domnop0  10990  fstwrdne  11032  elovmpowrd  11035  lswlgt0cl  11045  ccatrn  11065  swrdnd  11112  recvguniq  11306  abs00ap  11373  absext  11374  absnid  11384  cau3lem  11425  climuni  11604  2clim  11612  summodc  11694  fisumss  11703  fsumabs  11776  mertenslem2  11847  fprodssdc  11901  reeff1  12011  efieq1re  12083  dvdsmultr2  12144  dvdsleabs  12156  odd2np1lem  12183  odd2np1  12184  ltoddhalfle  12204  halfleoddlt  12205  m1expo  12211  nn0enne  12213  nn0ehalf  12214  nn0o1gt2  12216  flodddiv4  12247  zeqzmulgcd  12291  gcdneg  12303  gcdaddm  12305  bezoutlemaz  12324  bezoutlembz  12325  dfgcd2  12335  gcddiv  12340  dvdssqim  12345  algcvgblem  12371  algcvga  12373  lcmneg  12396  coprmgcdb  12410  coprmdvds2  12415  qredeq  12418  divgcdcoprm0  12423  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  prmind2  12442  dvdsnprmd  12447  prmgt1  12454  nprmdvds1  12462  divgcdodd  12465  euclemma  12468  prmdvdsexpr  12472  prmfac1  12474  prmndvdsfaclt  12478  crth  12546  eulerthlemh  12553  fermltl  12556  nnnn0modprm0  12578  coprimeprodsq2  12581  pythagtriplem2  12589  pcpremul  12616  pcdvdsb  12643  pc2dvds  12653  pc11  12654  dvdsprmpweqnn  12659  dvdsprmpweqle  12660  difsqpwdvds  12661  pcfac  12673  oddprmdvds  12677  prmpwdvds  12678  1arith  12690  4sqlem11  12724  4sqlem12  12725  imasaddfnlemg  13146  erlecpbl  13164  xpsff1o  13181  imasmnd2  13284  grp1inv  13439  imasgrp2  13446  ghmpreima  13602  imasabl  13672  imasrng  13718  imasring  13826  dvdsrtr  13863  dvdsrmul1  13864  unitgrp  13878  znidomb  14420  tgtop  14540  tgidm  14546  neipsm  14626  restbasg  14640  tgrest  14641  tgcn  14680  tgcnp  14681  cnconst2  14705  cnconst  14706  cnptopresti  14710  txbasval  14739  txcnp  14743  txdis1cn  14750  bldisj  14873  xblm  14889  blssps  14899  blss  14900  blin2  14904  cnlimcim  15143  dveflem  15198  sincosq3sgn  15300  sincosq4sgn  15301  coseq0q4123  15306  ioocosf1o  15326  logbgcd1irr  15439  mpodvdsmulf1o  15462  zabsle1  15476  lgsdir2lem5  15509  lgsne0  15515  lgsdirnn0  15524  gausslemma2dlem0i  15534  gausslemma2dlem1a  15535  gausslemma2dlem2  15539  gausslemma2dlem7  15545  gausslemma2d  15546  lgseisenlem2  15548  lgsquadlem1  15554  2lgslem1a1  15563  2lgslem1b  15566  2lgslem1c  15567  2lgs  15581  2lgsoddprmlem2  15583  uzdcinzz  15734  subctctexmid  15937