Theorem sylbird 259

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr3d  292  ceqex  3639  eqreu  3724  sotr2  5619  sotr3  5626  sossfld  6184  ordintdif  6413  tz6.12i  6918  f1cofveqaeqALT  7260  soisoi  7327  riotaeqimp  7394  ov3  7572  tfindsg  7852  tfindsg2  7853  nnsuc  7875  findsg  7892  soseq  8147  suppssr  8183  suppssrg  8184  tfrlem9  8387  oe0lem  8515  oa00  8561  omwordi  8573  om00  8577  omass  8582  oelim2  8597  oeoa  8599  oeoe  8601  nnmwordi  8637  swoso  8738  dom2lem  8990  onsdominel  9128  f1finf1o  9273  f1finf1oOLD  9274  cantnfp1lem3  9677  cantnfp1  9678  cantnflem1  9686  ttrclselem2  9723  rankr1ai  9795  rankval3b  9823  harcard  9975  infxpenlem  10010  alephnbtwn  10068  alephinit  10092  infxp  10212  cofsmo  10266  infpssALT  10310  fin23lem24  10319  fin56  10390  ttukeylem6  10511  ficard  10562  alephval2  10569  fpwwe2lem7  10634  fpwwe2  10640  gchdju1  10653  pwfseqlem3  10657  pwfseqlem4a  10658  pwfseqlem4  10659  gchpwdom  10667  tskss  10755  inar1  10772  gruss  10793  gruurn  10795  ltsonq  10966  distrlem4pr  11023  sqgt0sr  11103  map2psrpr  11107  letric  11318  renegcli  11525  addid0  11637  mulge0b  12088  nnge1  12244  0mnnnnn0  12508  nn0lt2  12629  zneo  12649  uzind2  12659  fzind  12664  nn0ind-raph  12666  uzwo  12899  nn01to3  12929  zbtwnre  12934  rpnnen1lem5  12969  ledivge1le  13049  xrletri  13136  qsqueeze  13184  difreicc  13465  elfzmlbp  13616  difelfznle  13619  elfzodifsumelfzo  13702  ssfzo12  13729  elfzonelfzo  13738  flflp1  13776  fleqceilz  13823  modsumfzodifsn  13913  addmodlteq  13915  om2uzf1oi  13922  expnngt1  14208  facdiv  14251  facwordi  14253  bcpasc  14285  hashdom  14343  hashgt23el  14388  hashdmpropge2  14448  ccatsymb  14536  swrdnnn0nd  14610  swrdnd0  14611  swrdsbslen  14618  swrdspsleq  14619  swrdlsw  14621  pfxnd0  14642  swrdswrdlem  14658  swrdccatin1  14679  pfxccatin12lem3  14686  swrdccat  14689  pfxccat3a  14692  repswswrd  14738  cshwidx0  14760  cshwcsh2id  14783  limsupbnd1  15430  lo1bdd2  15472  addcn2  15542  mulcn2  15544  o1rlimmul  15567  lo1add  15575  lo1mul  15576  rlimno1  15604  ruclem3  16180  odd2np1  16288  oddge22np1  16296  bitsfzo  16380  cncongr1  16608  2mulprm  16634  prm23ge5  16752  pcdvdsb  16806  pcaddlem  16825  infpnlem1  16847  prmunb  16851  vdwlem9  16926  vdwnnlem3  16934  ramcl  16966  prmgaplem5  16992  cshwshash  17042  setcmon  18041  setcepi  18042  setciso  18045  xpsmnd0  18700  f1ghm0to0  19159  ghmf1  19160  sylow2alem2  19527  sylow2blem3  19531  qusabl  19774  lt6abl  19804  cyggexb  19808  gsumcom2  19884  ringurd  20079  imasring  20218  xpsring1d  20221  0ring1eq0  20422  subrgdvds  20476  drnginvrcl  20522  drnginvrl  20525  drnginvrr  20526  lsmelval2  20840  quscrng  21029  isdomn4  21118  xrsdsreclblem  21191  obs2ss  21503  obslbs  21504  rnasclassa  21668  mplsubrglem  21782  gsummoncoe1  22048  mp2pm2mplem4  22531  chfacfisf  22576  chfacfisfcpmat  22577  cayleyhamilton1  22614  cmpsublem  23123  cmpsub  23124  1stccnp  23186  locfincf  23255  txhaus  23371  xkohaus  23377  ufilss  23629  cfinufil  23652  fmfnfmlem1  23678  hausflim  23705  fclscf  23749  alexsubb  23770  qustgplem  23845  prdsbl  24220  metss2lem  24240  nghmcn  24482  cfil3i  25017  cmetcaulem  25036  minveclem4  25180  ovolgelb  25229  ovolunnul  25249  ovoliun  25254  ovoliunnul  25256  ovolicc2lem2  25267  iundisj2  25298  voliunlem3  25301  rolle  25742  dvlip  25745  lhop1lem  25765  lhop2  25767  dvfsumrlim  25783  deg1ge  25851  coeeulem  25973  dgrco  26025  radcnvlt1  26166  psercnlem1  26173  logcnlem2  26387  logcnlem3  26388  cxpeq  26501  angpined  26571  efrlim  26710  dmgmaddn0  26763  lgamucov  26778  basellem2  26822  ppieq0  26916  mumullem2  26920  chpeq0  26947  chteq0  26948  chtub  26951  fsumvma  26952  dchrptlem1  27003  bposlem6  27028  gausslemma2dlem0i  27103  gausslemma2dlem1a  27104  lgseisenlem2  27115  2sqlem6  27162  2sq2  27172  2sqnn0  27177  2sqreulem1  27185  2sqreunnlem1  27188  dchrisum0lem1  27255  pntrsumbnd2  27306  pntlem3  27348  noextenddif  27407  nosupno  27442  nosupbnd1  27453  noinfno  27457  noinfbnd1  27468  noetasuplem4  27475  noetainflem4  27479  scutun12  27548  slerec  27557  cutlt  27657  sleadd2im  27710  colinearalg  28435  eengtrkg  28511  incistruhgr  28606  wlkv0  29175  crctcshwlkn0  29342  clwwlkccatlem  29509  clwlkclwwlklem2a4  29517  clwlkclwwlklem2  29520  clwlkclwwlkfo  29529  eucrctshift  29763  frrusgrord0  29860  frgrreg  29914  blocni  30325  ubthlem1  30390  minvecolem4  30400  shmodsi  30909  atcvati  31906  atcvat2i  31907  chirredlem4  31913  atmd2  31920  sumdmdlem  31938  addltmulALT  31966  iundisj2f  32088  iundisj2fi  32275  f1resveqaeq  34386  erdszelem9  34488  satffunlem1lem2  34692  satffunlem2lem2  34695  rdgprc  35070  cgrsub  35321  btwnxfr  35332  lineext  35352  linecgr  35357  btwnconn1lem4  35366  btwnconn1lem5  35367  btwnconn1lem6  35368  btwnconn1lem8  35370  btwnconn1lem11  35373  mptsnunlem  36522  finxpreclem6  36580  ltflcei  36779  poimirlem23  36814  poimirlem24  36815  poimirlem31  36822  poimirlem32  36823  ftc1anclem5  36868  heiborlem6  36987  grpokerinj  37064  dvrunz  37125  isdmn3  37245  dmncan1  37247  membpartlem19  37984  l1cvpat  38227  atnle  38490  cvlexch3  38505  cvlexch4N  38506  cvlatexchb1  38507  cvrat2  38603  atlelt  38612  3dimlem4a  38637  3dimlem4OLDN  38639  ps-1  38651  ps-2  38652  4atlem10  38780  4atlem11  38783  4atlem12  38786  cdleme11c  39435  cdleme21c  39501  cdlemg6d  39795  trlcoat  39897  tendoid0  39999  cdleml3N  40152  dia2dimlem7  40244  metakunt1  41291  metakunt6  41296  fsuppind  41464  pellexlem1  41869  pellexlem6  41874  imasgim  42144  onsupmaxb  42290  safesnsupfidom1o  42470  reabsifnpos  42686  reabsifnneg  42688  iunrelexpmin1  42761  iunrelexpmin2  42765  radcnvrat  43375  nzss  43378  elprneb  46037  or2expropbi  46042  tz6.12i-afv2  46249  dfatcolem  46261  f1oresf1o2  46297  zm1nn  46308  2ffzoeq  46334  sfprmdvdsmersenne  46569  lighneallem3  46573  lighneallem4  46576  requad01  46587  fppr2odd  46697  fpprwppr  46705  stgoldbwt  46742  sbgoldbaltlem1  46745  isomuspgrlem1  46793  lmod0rng  46908  lidldomn1  46911  rngciso  46968  rngcisoALTV  46980  ringciso  47019  ringcisoALTV  47043  ztprmneprm  47111  lincresunit3  47249  itsclc0yqsol  47537  itschlc0xyqsol1  47539  aacllem  47935