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  3595  eqreu  3676  sotr2  5566  sotr3  5573  sossfld  6144  ordintdif  6368  tz6.12i  6860  f1cofveqaeqALT  7206  soisoi  7276  riotaeqimp  7343  ov3  7523  tfindsg  7805  tfindsg2  7806  nnsuc  7828  findsg  7841  soseq  8102  suppssr  8138  suppssrg  8139  tfrlem9  8317  oe0lem  8441  oa00  8487  omwordi  8499  om00  8503  omass  8508  oelim2  8524  oeoa  8526  oeoe  8528  nnmwordi  8564  swoso  8671  dom2lem  8932  onsdominel  9057  f1finf1o  9176  fiint  9230  cantnfp1lem3  9592  cantnfp1  9593  cantnflem1  9601  ttrclselem2  9638  rankr1ai  9713  rankval3b  9741  harcard  9893  infxpenlem  9926  alephnbtwn  9984  alephinit  10008  infxp  10127  cofsmo  10182  infpssALT  10226  fin23lem24  10235  fin56  10306  ttukeylem6  10427  ficard  10478  alephval2  10486  fpwwe2lem7  10551  fpwwe2  10557  gchdju1  10570  pwfseqlem3  10574  pwfseqlem4a  10575  pwfseqlem4  10576  gchpwdom  10584  tskss  10672  inar1  10689  gruss  10710  gruurn  10712  ltsonq  10883  distrlem4pr  10940  sqgt0sr  11020  map2psrpr  11024  letric  11237  renegcli  11446  addid0  11560  mulge0b  12017  nnge1  12196  0mnnnnn0  12460  nn0lt2  12583  zneo  12603  uzind2  12613  fzind  12618  nn0ind-raph  12620  uzwo  12852  nn01to3  12882  zbtwnre  12887  rpnnen1lem5  12922  ledivge1le  13006  xrletri  13095  qsqueeze  13144  difreicc  13428  elfzmlbp  13584  difelfznle  13587  elfzodifsumelfzo  13677  ssfzo12  13705  elfzonelfzo  13715  flflp1  13757  fleqceilz  13804  modsumfzodifsn  13897  addmodlteq  13899  om2uzf1oi  13906  expnngt1  14194  facdiv  14240  facwordi  14242  bcpasc  14274  hashdom  14332  hashgt23el  14377  hashdmpropge2  14436  ccatsymb  14536  swrdnnn0nd  14610  swrdnd0  14611  swrdsbslen  14618  swrdspsleq  14619  swrdlsw  14621  pfxnd0  14642  swrdswrdlem  14657  swrdccatin1  14678  pfxccatin12lem3  14685  swrdccat  14688  pfxccat3a  14691  repswswrd  14737  cshwidx0  14759  cshwcsh2id  14781  limsupbnd1  15435  lo1bdd2  15477  addcn2  15547  mulcn2  15549  o1rlimmul  15572  lo1add  15580  lo1mul  15581  rlimno1  15607  ruclem3  16191  odd2np1  16301  oddge22np1  16309  bitsfzo  16395  cncongr1  16627  2mulprm  16653  prm23ge5  16777  pcdvdsb  16831  pcaddlem  16850  infpnlem1  16872  prmunb  16876  vdwlem9  16951  vdwnnlem3  16959  ramcl  16991  prmgaplem5  17017  cshwshash  17066  setcmon  18045  setcepi  18046  setciso  18049  xpsmnd0  18737  f1ghm0to0  19211  ghmf1  19212  sylow2alem2  19584  sylow2blem3  19588  qusabl  19831  lt6abl  19861  cyggexb  19865  gsumcom2  19941  ringurd  20157  imasring  20301  xpsring1d  20304  0ring1eq0  20501  subrgdvds  20554  rngciso  20606  ringciso  20640  isdomn4  20684  drnginvrcl  20721  drnginvrl  20724  drnginvrr  20725  lsmelval2  21072  quscrng  21273  xrsdsreclblem  21402  obs2ss  21719  obslbs  21720  rnasclassa  21885  mplsubrglem  21992  psdmul  22142  gsummoncoe1  22283  mp2pm2mplem4  22784  chfacfisf  22829  chfacfisfcpmat  22830  cayleyhamilton1  22867  cmpsublem  23374  cmpsub  23375  1stccnp  23437  locfincf  23506  txhaus  23622  xkohaus  23628  ufilss  23880  cfinufil  23903  fmfnfmlem1  23929  hausflim  23956  fclscf  24000  alexsubb  24021  qustgplem  24096  prdsbl  24466  metss2lem  24486  nghmcn  24720  cfil3i  25246  cmetcaulem  25265  minveclem4  25409  ovolgelb  25457  ovolunnul  25477  ovoliun  25482  ovoliunnul  25484  ovolicc2lem2  25495  iundisj2  25526  voliunlem3  25529  rolle  25967  dvlip  25970  lhop1lem  25990  lhop2  25992  dvfsumrlim  26008  deg1ge  26073  coeeulem  26199  dgrco  26250  radcnvlt1  26396  psercnlem1  26403  logcnlem2  26620  logcnlem3  26621  cxpeq  26734  angpined  26807  efrlim  26946  efrlimOLD  26947  dmgmaddn0  27000  lgamucov  27015  basellem2  27059  ppieq0  27153  mumullem2  27157  chpeq0  27185  chteq0  27186  chtub  27189  fsumvma  27190  dchrptlem1  27241  bposlem6  27266  gausslemma2dlem0i  27341  gausslemma2dlem1a  27342  lgseisenlem2  27353  2sqlem6  27400  2sq2  27410  2sqnn0  27415  2sqreulem1  27423  2sqreunnlem1  27426  dchrisum0lem1  27493  pntrsumbnd2  27544  pntlem3  27586  noextenddif  27646  nosupno  27681  nosupbnd1  27692  noinfno  27696  noinfbnd1  27707  noetasuplem4  27714  noetainflem4  27718  cutsun12  27796  lesrec  27805  cutlt  27938  leadds2im  27994  oniso  28277  n0fincut  28361  bdayfinbndlem1  28473  z12bdaylem1  28476  colinearalg  28993  eengtrkg  29069  incistruhgr  29162  wlkv0  29733  crctcshwlkn0  29904  clwwlkccatlem  30074  clwlkclwwlklem2a4  30082  clwlkclwwlklem2  30085  clwlkclwwlkfo  30094  eucrctshift  30328  frrusgrord0  30425  frgrreg  30479  blocni  30891  ubthlem1  30956  minvecolem4  30966  shmodsi  31475  atcvati  32472  atcvat2i  32473  chirredlem4  32479  atmd2  32486  sumdmdlem  32504  addltmulALT  32532  iundisj2f  32675  iundisj2fi  32885  f1resveqaeq  35244  erdszelem9  35397  satffunlem1lem2  35601  satffunlem2lem2  35604  rdgprc  35990  cgrsub  36243  btwnxfr  36254  lineext  36274  linecgr  36279  btwnconn1lem4  36288  btwnconn1lem5  36289  btwnconn1lem6  36290  btwnconn1lem8  36292  btwnconn1lem11  36295  mh-inf3f1  36739  mptsnunlem  37668  finxpreclem6  37726  ltflcei  37943  poimirlem23  37978  poimirlem24  37979  poimirlem31  37986  poimirlem32  37987  ftc1anclem5  38032  heiborlem6  38151  grpokerinj  38228  dvrunz  38289  isdmn3  38409  dmncan1  38411  membpartlem19  39249  l1cvpat  39514  atnle  39777  cvlexch3  39792  cvlexch4N  39793  cvlatexchb1  39794  cvrat2  39889  atlelt  39898  3dimlem4a  39923  3dimlem4OLDN  39925  ps-1  39937  ps-2  39938  4atlem10  40066  4atlem11  40069  4atlem12  40072  cdleme11c  40721  cdleme21c  40787  cdlemg6d  41081  trlcoat  41183  tendoid0  41285  cdleml3N  41438  dia2dimlem7  41530  aks6d1c6lem3  42625  expeq1d  42770  fsuppind  43037  pellexlem1  43275  pellexlem6  43280  imasgim  43546  onsupmaxb  43685  safesnsupfidom1o  43862  reabsifnpos  44078  reabsifnneg  44080  iunrelexpmin1  44153  iunrelexpmin2  44157  radcnvrat  44759  nzss  44762  pwclaxpow  45429  ormkglobd  47321  elprneb  47489  or2expropbi  47494  tz6.12i-afv2  47703  dfatcolem  47715  f1oresf1o2  47751  zm1nn  47762  2ffzoeq  47788  modmkpkne  47827  sfprmdvdsmersenne  48078  lighneallem3  48082  lighneallem4  48085  requad01  48109  fppr2odd  48219  fpprwppr  48227  stgoldbwt  48264  sbgoldbaltlem1  48267  isuspgrimlem  48383  upgrimpthslem2  48396  isubgr3stgrlem4  48457  isubgr3stgrlem7  48460  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem3  48561  lmod0rng  48717  lidldomn1  48719  rngcisoALTV  48765  ringcisoALTV  48799  ztprmneprm  48835  lincresunit3  48969  itsclc0yqsol  49252  itschlc0xyqsol1  49254  aacllem  50288