Theorem sylbird 260

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 248	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr3d  293  ceqex  3652  eqreu  3735  sotr2  5626  sotr3  5633  sossfld  6206  ordintdif  6434  tz6.12i  6934  f1cofveqaeqALT  7279  soisoi  7348  riotaeqimp  7414  ov3  7596  tfindsg  7882  tfindsg2  7883  nnsuc  7905  findsg  7919  soseq  8184  suppssr  8220  suppssrg  8221  tfrlem9  8425  oe0lem  8551  oa00  8597  omwordi  8609  om00  8613  omass  8618  oelim2  8633  oeoa  8635  oeoe  8637  nnmwordi  8673  swoso  8779  dom2lem  9032  onsdominel  9166  f1finf1o  9305  f1finf1oOLD  9306  fiint  9366  cantnfp1lem3  9720  cantnfp1  9721  cantnflem1  9729  ttrclselem2  9766  rankr1ai  9838  rankval3b  9866  harcard  10018  infxpenlem  10053  alephnbtwn  10111  alephinit  10135  infxp  10254  cofsmo  10309  infpssALT  10353  fin23lem24  10362  fin56  10433  ttukeylem6  10554  ficard  10605  alephval2  10612  fpwwe2lem7  10677  fpwwe2  10683  gchdju1  10696  pwfseqlem3  10700  pwfseqlem4a  10701  pwfseqlem4  10702  gchpwdom  10710  tskss  10798  inar1  10815  gruss  10836  gruurn  10838  ltsonq  11009  distrlem4pr  11066  sqgt0sr  11146  map2psrpr  11150  letric  11361  renegcli  11570  addid0  11682  mulge0b  12138  nnge1  12294  0mnnnnn0  12558  nn0lt2  12681  zneo  12701  uzind2  12711  fzind  12716  nn0ind-raph  12718  uzwo  12953  nn01to3  12983  zbtwnre  12988  rpnnen1lem5  13023  ledivge1le  13106  xrletri  13195  qsqueeze  13243  difreicc  13524  elfzmlbp  13679  difelfznle  13682  elfzodifsumelfzo  13770  ssfzo12  13798  elfzonelfzo  13808  flflp1  13847  fleqceilz  13894  modsumfzodifsn  13985  addmodlteq  13987  om2uzf1oi  13994  expnngt1  14280  facdiv  14326  facwordi  14328  bcpasc  14360  hashdom  14418  hashgt23el  14463  hashdmpropge2  14522  ccatsymb  14620  swrdnnn0nd  14694  swrdnd0  14695  swrdsbslen  14702  swrdspsleq  14703  swrdlsw  14705  pfxnd0  14726  swrdswrdlem  14742  swrdccatin1  14763  pfxccatin12lem3  14770  swrdccat  14773  pfxccat3a  14776  repswswrd  14822  cshwidx0  14844  cshwcsh2id  14867  limsupbnd1  15518  lo1bdd2  15560  addcn2  15630  mulcn2  15632  o1rlimmul  15655  lo1add  15663  lo1mul  15664  rlimno1  15690  ruclem3  16269  odd2np1  16378  oddge22np1  16386  bitsfzo  16472  cncongr1  16704  2mulprm  16730  prm23ge5  16853  pcdvdsb  16907  pcaddlem  16926  infpnlem1  16948  prmunb  16952  vdwlem9  17027  vdwnnlem3  17035  ramcl  17067  prmgaplem5  17093  cshwshash  17142  setcmon  18132  setcepi  18133  setciso  18136  xpsmnd0  18791  f1ghm0to0  19263  ghmf1  19264  sylow2alem2  19636  sylow2blem3  19640  qusabl  19883  lt6abl  19913  cyggexb  19917  gsumcom2  19993  ringurd  20182  imasring  20327  xpsring1d  20330  0ring1eq0  20533  subrgdvds  20586  rngciso  20638  ringciso  20672  isdomn4  20716  drnginvrcl  20753  drnginvrl  20756  drnginvrr  20757  lsmelval2  21084  quscrng  21293  xrsdsreclblem  21430  obs2ss  21749  obslbs  21750  rnasclassa  21915  mplsubrglem  22024  psdmul  22170  gsummoncoe1  22312  mp2pm2mplem4  22815  chfacfisf  22860  chfacfisfcpmat  22861  cayleyhamilton1  22898  cmpsublem  23407  cmpsub  23408  1stccnp  23470  locfincf  23539  txhaus  23655  xkohaus  23661  ufilss  23913  cfinufil  23936  fmfnfmlem1  23962  hausflim  23989  fclscf  24033  alexsubb  24054  qustgplem  24129  prdsbl  24504  metss2lem  24524  nghmcn  24766  cfil3i  25303  cmetcaulem  25322  minveclem4  25466  ovolgelb  25515  ovolunnul  25535  ovoliun  25540  ovoliunnul  25542  ovolicc2lem2  25553  iundisj2  25584  voliunlem3  25587  rolle  26028  dvlip  26032  lhop1lem  26052  lhop2  26054  dvfsumrlim  26072  deg1ge  26137  coeeulem  26263  dgrco  26315  radcnvlt1  26461  psercnlem1  26469  logcnlem2  26685  logcnlem3  26686  cxpeq  26800  angpined  26873  efrlim  27012  efrlimOLD  27013  dmgmaddn0  27066  lgamucov  27081  basellem2  27125  ppieq0  27219  mumullem2  27223  chpeq0  27252  chteq0  27253  chtub  27256  fsumvma  27257  dchrptlem1  27308  bposlem6  27333  gausslemma2dlem0i  27408  gausslemma2dlem1a  27409  lgseisenlem2  27420  2sqlem6  27467  2sq2  27477  2sqnn0  27482  2sqreulem1  27490  2sqreunnlem1  27493  dchrisum0lem1  27560  pntrsumbnd2  27611  pntlem3  27653  noextenddif  27713  nosupno  27748  nosupbnd1  27759  noinfno  27763  noinfbnd1  27774  noetasuplem4  27781  noetainflem4  27785  scutun12  27855  slerec  27864  cutlt  27966  sleadd2im  28021  colinearalg  28925  eengtrkg  29001  incistruhgr  29096  wlkv0  29669  crctcshwlkn0  29841  clwwlkccatlem  30008  clwlkclwwlklem2a4  30016  clwlkclwwlklem2  30019  clwlkclwwlkfo  30028  eucrctshift  30262  frrusgrord0  30359  frgrreg  30413  blocni  30824  ubthlem1  30889  minvecolem4  30899  shmodsi  31408  atcvati  32405  atcvat2i  32406  chirredlem4  32412  atmd2  32419  sumdmdlem  32437  addltmulALT  32465  iundisj2f  32603  iundisj2fi  32799  f1resveqaeq  35099  erdszelem9  35204  satffunlem1lem2  35408  satffunlem2lem2  35411  rdgprc  35795  cgrsub  36046  btwnxfr  36057  lineext  36077  linecgr  36082  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem8  36095  btwnconn1lem11  36098  mptsnunlem  37339  finxpreclem6  37397  ltflcei  37615  poimirlem23  37650  poimirlem24  37651  poimirlem31  37658  poimirlem32  37659  ftc1anclem5  37704  heiborlem6  37823  grpokerinj  37900  dvrunz  37961  isdmn3  38081  dmncan1  38083  membpartlem19  38812  l1cvpat  39055  atnle  39318  cvlexch3  39333  cvlexch4N  39334  cvlatexchb1  39335  cvrat2  39431  atlelt  39440  3dimlem4a  39465  3dimlem4OLDN  39467  ps-1  39479  ps-2  39480  4atlem10  39608  4atlem11  39611  4atlem12  39614  cdleme11c  40263  cdleme21c  40329  cdlemg6d  40623  trlcoat  40725  tendoid0  40827  cdleml3N  40980  dia2dimlem7  41072  aks6d1c6lem3  42173  metakunt1  42206  metakunt6  42211  expeq1d  42359  fsuppind  42600  pellexlem1  42840  pellexlem6  42845  imasgim  43112  onsupmaxb  43251  safesnsupfidom1o  43430  reabsifnpos  43646  reabsifnneg  43648  iunrelexpmin1  43721  iunrelexpmin2  43725  radcnvrat  44333  nzss  44336  pwclaxpow  45001  ormkglobd  46890  elprneb  47041  or2expropbi  47046  tz6.12i-afv2  47255  dfatcolem  47267  f1oresf1o2  47303  zm1nn  47314  2ffzoeq  47339  sfprmdvdsmersenne  47590  lighneallem3  47594  lighneallem4  47597  requad01  47608  fppr2odd  47718  fpprwppr  47726  stgoldbwt  47763  sbgoldbaltlem1  47766  isuspgrimlem  47874  isubgr3stgrlem4  47936  isubgr3stgrlem7  47939  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem3  48029  lmod0rng  48145  lidldomn1  48147  rngcisoALTV  48193  ringcisoALTV  48227  ztprmneprm  48263  lincresunit3  48398  itsclc0yqsol  48685  itschlc0xyqsol1  48687  aacllem  49320