Theorem sylbird 262

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbird.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
sylbird.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylbird	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 250	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  3imtr3d  295  ceqex  3645  eqreu  3720  sotr2  5505  sossfld  6043  ordintdif  6240  tz6.12i  6696  f1cofveqaeqALT  7017  soisoi  7081  riotaeqimp  7140  ov3  7311  tfindsg  7575  tfindsg2  7576  nnsuc  7597  findsg  7609  suppssr  7861  tfrlem9  8021  oe0lem  8138  oa00  8185  omwordi  8197  om00  8201  omass  8206  oelim2  8221  oeoa  8223  oeoe  8225  nnmwordi  8261  swoso  8322  dom2lem  8549  onsdominel  8666  f1finf1o  8745  cantnfp1lem3  9143  cantnfp1  9144  cantnflem1  9152  rankr1ai  9227  rankval3b  9255  harcard  9407  infxpenlem  9439  alephnbtwn  9497  alephinit  9521  infxp  9637  cofsmo  9691  infpssALT  9735  fin23lem24  9744  fin56  9815  ttukeylem6  9936  ficard  9987  alephval2  9994  fpwwe2lem8  10059  fpwwe2  10065  gchdju1  10078  pwfseqlem3  10082  pwfseqlem4a  10083  pwfseqlem4  10084  gchpwdom  10092  tskss  10180  inar1  10197  gruss  10218  gruurn  10220  ltsonq  10391  distrlem4pr  10448  sqgt0sr  10528  map2psrpr  10532  letric  10740  renegcli  10947  addid0  11059  mulge0b  11510  nnge1  11666  0mnnnnn0  11930  nn0lt2  12046  zneo  12066  uzind2  12076  fzind  12081  nn0ind-raph  12083  uzwo  12312  nn01to3  12342  zbtwnre  12347  rpnnen1lem5  12381  ledivge1le  12461  xrletri  12547  qsqueeze  12595  difreicc  12871  elfzmlbp  13019  difelfznle  13022  elfzodifsumelfzo  13104  ssfzo12  13131  elfzonelfzo  13140  flflp1  13178  fleqceilz  13223  modsumfzodifsn  13313  addmodlteq  13315  om2uzf1oi  13322  expnngt1  13603  facdiv  13648  facwordi  13650  bcpasc  13682  hashdom  13741  hashgt23el  13786  hashdmpropge2  13842  ccatsymb  13936  swrdnnn0nd  14018  swrdnd0  14019  swrdsbslen  14026  swrdspsleq  14027  swrdlsw  14029  pfxnd0  14050  swrdswrdlem  14066  swrdccatin1  14087  pfxccatin12lem3  14094  swrdccat  14097  pfxccat3a  14100  repswswrd  14146  cshwidx0  14168  cshwcsh2id  14190  limsupbnd1  14839  lo1bdd2  14881  addcn2  14950  mulcn2  14952  o1rlimmul  14975  lo1add  14983  lo1mul  14984  rlimno1  15010  ruclem3  15586  odd2np1  15690  oddge22np1  15698  bitsfzo  15784  cncongr1  16011  2mulprm  16037  prm23ge5  16152  pcdvdsb  16205  pcaddlem  16224  infpnlem1  16246  prmunb  16250  vdwlem9  16325  vdwnnlem3  16333  ramcl  16365  prmgaplem5  16391  cshwshash  16438  setcmon  17347  setcepi  17348  setciso  17351  ghmf1  18387  sylow2alem2  18743  sylow2blem3  18747  qusabl  18985  lt6abl  19015  cyggexb  19019  gsumcom2  19095  imasring  19369  f1ghm0to0  19492  f1rhm0to0OLD  19493  drnginvrcl  19519  drnginvrl  19521  drnginvrr  19522  subrgdvds  19549  lsmelval2  19857  quscrng  20013  rnasclassa  20124  mplsubrglem  20219  gsummoncoe1  20472  xrsdsreclblem  20591  obs2ss  20873  obslbs  20874  mp2pm2mplem4  21417  chfacfisf  21462  chfacfisfcpmat  21463  cayleyhamilton1  21500  cmpsublem  22007  cmpsub  22008  1stccnp  22070  locfincf  22139  txhaus  22255  xkohaus  22261  ufilss  22513  cfinufil  22536  fmfnfmlem1  22562  hausflim  22589  fclscf  22633  alexsubb  22654  qustgplem  22729  prdsbl  23101  metss2lem  23121  nghmcn  23354  cfil3i  23872  cmetcaulem  23891  minveclem4  24035  ovolgelb  24081  ovolunnul  24101  ovoliun  24106  ovoliunnul  24108  ovolicc2lem2  24119  iundisj2  24150  voliunlem3  24153  rolle  24587  dvlip  24590  lhop1lem  24610  lhop2  24612  dvfsumrlim  24628  deg1ge  24692  coeeulem  24814  dgrco  24865  radcnvlt1  25006  psercnlem1  25013  logcnlem2  25226  logcnlem3  25227  cxpeq  25338  angpined  25408  efrlim  25547  dmgmaddn0  25600  lgamucov  25615  basellem2  25659  ppieq0  25753  mumullem2  25757  chpeq0  25784  chteq0  25785  chtub  25788  fsumvma  25789  dchrptlem1  25840  bposlem6  25865  gausslemma2dlem0i  25940  gausslemma2dlem1a  25941  lgseisenlem2  25952  2sqlem6  25999  2sq2  26009  2sqnn0  26014  2sqreulem1  26022  2sqreunnlem1  26025  dchrisum0lem1  26092  pntrsumbnd2  26143  pntlem3  26185  colinearalg  26696  eengtrkg  26772  incistruhgr  26864  wlkv0  27432  crctcshwlkn0  27599  clwwlkccatlem  27767  clwlkclwwlklem2a4  27775  clwlkclwwlklem2  27778  clwlkclwwlkfo  27787  eucrctshift  28022  frrusgrord0  28119  frgrreg  28173  blocni  28582  ubthlem1  28647  minvecolem4  28657  shmodsi  29166  atcvati  30163  atcvat2i  30164  chirredlem4  30170  atmd2  30177  sumdmdlem  30195  addltmulALT  30223  iundisj2f  30340  iundisj2fi  30520  rngurd  30857  f1resveqaeq  32358  erdszelem9  32446  satffunlem1lem2  32650  satffunlem2lem2  32653  sotr3  33002  rdgprc  33039  soseq  33096  noextenddif  33175  nosupno  33203  nosupbnd1  33214  noetalem3  33219  scutun12  33271  slerec  33277  cgrsub  33506  btwnxfr  33517  lineext  33537  linecgr  33542  btwnconn1lem4  33551  btwnconn1lem5  33552  btwnconn1lem6  33553  btwnconn1lem8  33555  btwnconn1lem11  33558  mptsnunlem  34622  finxpreclem6  34680  ltflcei  34895  poimirlem23  34930  poimirlem24  34931  poimirlem31  34938  poimirlem32  34939  ftc1anclem5  34986  heiborlem6  35109  grpokerinj  35186  dvrunz  35247  isdmn3  35367  dmncan1  35369  l1cvpat  36205  atnle  36468  cvlexch3  36483  cvlexch4N  36484  cvlatexchb1  36485  cvrat2  36580  atlelt  36589  3dimlem4a  36614  3dimlem4OLDN  36616  ps-1  36628  ps-2  36629  4atlem10  36757  4atlem11  36760  4atlem12  36763  cdleme11c  37412  cdleme21c  37478  cdlemg6d  37772  trlcoat  37874  tendoid0  37976  cdleml3N  38129  dia2dimlem7  38221  pellexlem1  39446  pellexlem6  39451  imasgim  39720  iunrelexpmin1  40073  iunrelexpmin2  40077  radcnvrat  40666  nzss  40669  elprneb  43284  or2expropbi  43289  tz6.12i-afv2  43462  dfatcolem  43474  f1oresf1o2  43510  zm1nn  43522  2ffzoeq  43548  sfprmdvdsmersenne  43788  lighneallem3  43792  lighneallem4  43795  requad01  43806  fppr2odd  43916  fpprwppr  43924  stgoldbwt  43961  sbgoldbaltlem1  43964  isomuspgrlem1  44012  lmod0rng  44159  0ring1eq0  44163  lidldomn1  44212  rngciso  44273  rngcisoALTV  44285  ringciso  44324  ringcisoALTV  44348  ztprmneprm  44415  lincresunit3  44556  itsclc0yqsol  44771  itschlc0xyqsol1  44773  aacllem  44922