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  3648  ssprsseq  3830  nlimsucg  4658  ssrelrn  4914  poltletr  5129  xp11m  5167  fvmptdf  5724  elfvmptrab1  5731  eusvobj2  5993  ovmpodf  6142  elovmporab  6211  elovmporab1w  6212  f1o2ndf1  6380  smoiso  6454  nnsseleq  6655  ecopovtrn  6787  ecopovtrng  6790  dom2lem  6931  fundmen  6967  dom1o  6985  fidifsnen  7040  findcard2  7059  findcard2s  7060  supisoex  7187  infglbti  7203  ordiso2  7213  updjud  7260  difinfsnlem  7277  enomnilem  7316  enmkvlem  7339  netap  7451  2omotaplemap  7454  cc2lem  7463  addcanpig  7532  mulcanpig  7533  addnidpig  7534  ordpipqqs  7572  ltexnqq  7606  prarloclemlo  7692  genpcdl  7717  genpcuu  7718  mulnqprl  7766  mulnqpru  7767  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  distrlem5prl  7784  distrlem5pru  7785  ltsopr  7794  ltexprlemfl  7807  ltexprlemfu  7809  recexprlemss1l  7833  recexprlemss1u  7834  aptiprleml  7837  ltsrprg  7945  lttrsr  7960  mulextsr1lem  7978  axapti  8228  cnegexlem1  8332  le2add  8602  lt2add  8603  ltleadd  8604  lt2sub  8618  le2sub  8619  recexre  8736  reapti  8737  apreap  8745  reapcotr  8756  remulext1  8757  apreim  8761  apcotr  8765  mulext2  8771  recexap  8811  addltmul  9359  elnnz  9467  zleloe  9504  difgtsumgt  9527  nn0n0n1ge2b  9537  nn0lt2  9539  nn0le2is012  9540  zextlt  9550  uzind2  9570  supinfneg  9802  infsupneg  9803  eluzdc  9817  qreccl  9849  elpq  9856  xltnegi  10043  xnn0lenn0nn0  10073  iccid  10133  icoshft  10198  zltaddlt1le  10215  fzofzim  10400  qbtwnxr  10489  flqeqceilz  10552  modqmuladdnn0  10602  modfzo0difsn  10629  addmodlteq  10632  frec2uzrand  10639  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  seqf1oglem1  10753  facdiv  10972  facwordi  10974  faclbnd  10975  bcpasc  11000  seq3coll  11077  fundm2domnop0  11080  fstwrdne  11123  elovmpowrd  11126  lswlgt0cl  11137  ccatrn  11157  ccatalpha  11161  swrdnd  11206  swrdswrd  11252  wrd2ind  11270  swrdccatin1  11272  pfxccatin12lem2a  11274  pfxccat3  11281  swrdccat  11282  swrdccat3blem  11286  reuccatpfxs1lem  11293  recvguniq  11521  abs00ap  11588  absext  11589  absnid  11599  cau3lem  11640  climuni  11819  2clim  11827  summodc  11909  fisumss  11918  fsumabs  11991  mertenslem2  12062  fprodssdc  12116  reeff1  12226  efieq1re  12298  dvdsmultr2  12359  dvdsleabs  12371  odd2np1lem  12398  odd2np1  12399  ltoddhalfle  12419  halfleoddlt  12420  m1expo  12426  nn0enne  12428  nn0ehalf  12429  nn0o1gt2  12431  flodddiv4  12462  zeqzmulgcd  12506  gcdneg  12518  gcdaddm  12520  bezoutlemaz  12539  bezoutlembz  12540  dfgcd2  12550  gcddiv  12555  dvdssqim  12560  algcvgblem  12586  algcvga  12588  lcmneg  12611  coprmgcdb  12625  coprmdvds2  12630  qredeq  12633  divgcdcoprm0  12638  divgcdcoprmex  12639  cncongr1  12640  cncongr2  12641  prmind2  12657  dvdsnprmd  12662  prmgt1  12669  nprmdvds1  12677  divgcdodd  12680  euclemma  12683  prmdvdsexpr  12687  prmfac1  12689  prmndvdsfaclt  12693  crth  12761  eulerthlemh  12768  fermltl  12771  nnnn0modprm0  12793  coprimeprodsq2  12796  pythagtriplem2  12804  pcpremul  12831  pcdvdsb  12858  pc2dvds  12868  pc11  12869  dvdsprmpweqnn  12874  dvdsprmpweqle  12875  difsqpwdvds  12876  pcfac  12888  oddprmdvds  12892  prmpwdvds  12893  1arith  12905  4sqlem11  12939  4sqlem12  12940  imasaddfnlemg  13362  erlecpbl  13380  xpsff1o  13397  imasmnd2  13500  grp1inv  13655  imasgrp2  13662  ghmpreima  13818  imasabl  13888  imasrng  13934  imasring  14042  dvdsrtr  14080  dvdsrmul1  14081  unitgrp  14095  znidomb  14637  tgtop  14757  tgidm  14763  neipsm  14843  restbasg  14857  tgrest  14858  tgcn  14897  tgcnp  14898  cnconst2  14922  cnconst  14923  cnptopresti  14927  txbasval  14956  txcnp  14960  txdis1cn  14967  bldisj  15090  xblm  15106  blssps  15116  blss  15117  blin2  15121  cnlimcim  15360  dveflem  15415  sincosq3sgn  15517  sincosq4sgn  15518  coseq0q4123  15523  ioocosf1o  15543  logbgcd1irr  15656  mpodvdsmulf1o  15679  zabsle1  15693  lgsdir2lem5  15726  lgsne0  15732  lgsdirnn0  15741  gausslemma2dlem0i  15751  gausslemma2dlem1a  15752  gausslemma2dlem2  15756  gausslemma2dlem7  15762  gausslemma2d  15763  lgseisenlem2  15765  lgsquadlem1  15771  2lgslem1a1  15780  2lgslem1b  15783  2lgslem1c  15784  2lgs  15798  2lgsoddprmlem2  15800  upgrpredgv  15959  ausgrumgrien  15983  ausgrusgrien  15984  usgruspgrben  15999  uhgr2edg  16019  usgredg4  16028  ushgredgedg  16039  ushgredgedgloop  16041  wlkl1loop  16099  wlk1walkdom  16100  wlklenvclwlk  16114  wlkres  16118  uzdcinzz  16217  subctctexmid  16425