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  3651  eqreu  3737  sotr2  5629  sotr3  5636  sossfld  6207  ordintdif  6435  tz6.12i  6934  f1cofveqaeqALT  7278  soisoi  7347  riotaeqimp  7413  ov3  7595  tfindsg  7881  tfindsg2  7882  nnsuc  7904  findsg  7919  soseq  8182  suppssr  8218  suppssrg  8219  tfrlem9  8423  oe0lem  8549  oa00  8595  omwordi  8607  om00  8611  omass  8616  oelim2  8631  oeoa  8633  oeoe  8635  nnmwordi  8671  swoso  8777  dom2lem  9030  onsdominel  9164  f1finf1o  9302  f1finf1oOLD  9303  fiint  9363  cantnfp1lem3  9717  cantnfp1  9718  cantnflem1  9726  ttrclselem2  9763  rankr1ai  9835  rankval3b  9863  harcard  10015  infxpenlem  10050  alephnbtwn  10108  alephinit  10132  infxp  10251  cofsmo  10306  infpssALT  10350  fin23lem24  10359  fin56  10430  ttukeylem6  10551  ficard  10602  alephval2  10609  fpwwe2lem7  10674  fpwwe2  10680  gchdju1  10693  pwfseqlem3  10697  pwfseqlem4a  10698  pwfseqlem4  10699  gchpwdom  10707  tskss  10795  inar1  10812  gruss  10833  gruurn  10835  ltsonq  11006  distrlem4pr  11063  sqgt0sr  11143  map2psrpr  11147  letric  11358  renegcli  11567  addid0  11679  mulge0b  12135  nnge1  12291  0mnnnnn0  12555  nn0lt2  12678  zneo  12698  uzind2  12708  fzind  12713  nn0ind-raph  12715  uzwo  12950  nn01to3  12980  zbtwnre  12985  rpnnen1lem5  13020  ledivge1le  13103  xrletri  13191  qsqueeze  13239  difreicc  13520  elfzmlbp  13675  difelfznle  13678  elfzodifsumelfzo  13766  ssfzo12  13794  elfzonelfzo  13804  flflp1  13843  fleqceilz  13890  modsumfzodifsn  13981  addmodlteq  13983  om2uzf1oi  13990  expnngt1  14276  facdiv  14322  facwordi  14324  bcpasc  14356  hashdom  14414  hashgt23el  14459  hashdmpropge2  14518  ccatsymb  14616  swrdnnn0nd  14690  swrdnd0  14691  swrdsbslen  14698  swrdspsleq  14699  swrdlsw  14701  pfxnd0  14722  swrdswrdlem  14738  swrdccatin1  14759  pfxccatin12lem3  14766  swrdccat  14769  pfxccat3a  14772  repswswrd  14818  cshwidx0  14840  cshwcsh2id  14863  limsupbnd1  15514  lo1bdd2  15556  addcn2  15626  mulcn2  15628  o1rlimmul  15651  lo1add  15659  lo1mul  15660  rlimno1  15686  ruclem3  16265  odd2np1  16374  oddge22np1  16382  bitsfzo  16468  cncongr1  16700  2mulprm  16726  prm23ge5  16848  pcdvdsb  16902  pcaddlem  16921  infpnlem1  16943  prmunb  16947  vdwlem9  17022  vdwnnlem3  17030  ramcl  17062  prmgaplem5  17088  cshwshash  17138  setcmon  18140  setcepi  18141  setciso  18144  xpsmnd0  18803  f1ghm0to0  19275  ghmf1  19276  sylow2alem2  19650  sylow2blem3  19654  qusabl  19897  lt6abl  19927  cyggexb  19931  gsumcom2  20007  ringurd  20202  imasring  20343  xpsring1d  20346  0ring1eq0  20549  subrgdvds  20602  rngciso  20654  ringciso  20688  isdomn4  20732  drnginvrcl  20769  drnginvrl  20772  drnginvrr  20773  lsmelval2  21101  quscrng  21310  xrsdsreclblem  21447  obs2ss  21766  obslbs  21767  rnasclassa  21932  mplsubrglem  22041  psdmul  22187  gsummoncoe1  22327  mp2pm2mplem4  22830  chfacfisf  22875  chfacfisfcpmat  22876  cayleyhamilton1  22913  cmpsublem  23422  cmpsub  23423  1stccnp  23485  locfincf  23554  txhaus  23670  xkohaus  23676  ufilss  23928  cfinufil  23951  fmfnfmlem1  23977  hausflim  24004  fclscf  24048  alexsubb  24069  qustgplem  24144  prdsbl  24519  metss2lem  24539  nghmcn  24781  cfil3i  25316  cmetcaulem  25335  minveclem4  25479  ovolgelb  25528  ovolunnul  25548  ovoliun  25553  ovoliunnul  25555  ovolicc2lem2  25566  iundisj2  25597  voliunlem3  25600  rolle  26042  dvlip  26046  lhop1lem  26066  lhop2  26068  dvfsumrlim  26086  deg1ge  26151  coeeulem  26277  dgrco  26329  radcnvlt1  26475  psercnlem1  26483  logcnlem2  26699  logcnlem3  26700  cxpeq  26814  angpined  26887  efrlim  27026  efrlimOLD  27027  dmgmaddn0  27080  lgamucov  27095  basellem2  27139  ppieq0  27233  mumullem2  27237  chpeq0  27266  chteq0  27267  chtub  27270  fsumvma  27271  dchrptlem1  27322  bposlem6  27347  gausslemma2dlem0i  27422  gausslemma2dlem1a  27423  lgseisenlem2  27434  2sqlem6  27481  2sq2  27491  2sqnn0  27496  2sqreulem1  27504  2sqreunnlem1  27507  dchrisum0lem1  27574  pntrsumbnd2  27625  pntlem3  27667  noextenddif  27727  nosupno  27762  nosupbnd1  27773  noinfno  27777  noinfbnd1  27788  noetasuplem4  27795  noetainflem4  27799  scutun12  27869  slerec  27878  cutlt  27980  sleadd2im  28035  colinearalg  28939  eengtrkg  29015  incistruhgr  29110  wlkv0  29683  crctcshwlkn0  29850  clwwlkccatlem  30017  clwlkclwwlklem2a4  30025  clwlkclwwlklem2  30028  clwlkclwwlkfo  30037  eucrctshift  30271  frrusgrord0  30368  frgrreg  30422  blocni  30833  ubthlem1  30898  minvecolem4  30908  shmodsi  31417  atcvati  32414  atcvat2i  32415  chirredlem4  32421  atmd2  32428  sumdmdlem  32446  addltmulALT  32474  iundisj2f  32609  iundisj2fi  32804  f1resveqaeq  35077  erdszelem9  35183  satffunlem1lem2  35387  satffunlem2lem2  35390  rdgprc  35775  cgrsub  36026  btwnxfr  36037  lineext  36057  linecgr  36062  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem8  36075  btwnconn1lem11  36078  mptsnunlem  37320  finxpreclem6  37378  ltflcei  37594  poimirlem23  37629  poimirlem24  37630  poimirlem31  37637  poimirlem32  37638  ftc1anclem5  37683  heiborlem6  37802  grpokerinj  37879  dvrunz  37940  isdmn3  38060  dmncan1  38062  membpartlem19  38792  l1cvpat  39035  atnle  39298  cvlexch3  39313  cvlexch4N  39314  cvlatexchb1  39315  cvrat2  39411  atlelt  39420  3dimlem4a  39445  3dimlem4OLDN  39447  ps-1  39459  ps-2  39460  4atlem10  39588  4atlem11  39591  4atlem12  39594  cdleme11c  40243  cdleme21c  40309  cdlemg6d  40603  trlcoat  40705  tendoid0  40807  cdleml3N  40960  dia2dimlem7  41052  aks6d1c6lem3  42153  metakunt1  42186  metakunt6  42191  expeq1d  42337  fsuppind  42576  pellexlem1  42816  pellexlem6  42821  imasgim  43088  onsupmaxb  43227  safesnsupfidom1o  43406  reabsifnpos  43622  reabsifnneg  43624  iunrelexpmin1  43697  iunrelexpmin2  43701  radcnvrat  44309  nzss  44312  elprneb  46978  or2expropbi  46983  tz6.12i-afv2  47192  dfatcolem  47204  f1oresf1o2  47240  zm1nn  47251  2ffzoeq  47276  sfprmdvdsmersenne  47527  lighneallem3  47531  lighneallem4  47534  requad01  47545  fppr2odd  47655  fpprwppr  47663  stgoldbwt  47700  sbgoldbaltlem1  47703  isuspgrimlem  47811  isubgr3stgrlem4  47871  isubgr3stgrlem7  47874  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem3  47963  lmod0rng  48072  lidldomn1  48074  rngcisoALTV  48120  ringcisoALTV  48154  ztprmneprm  48191  lincresunit3  48326  itsclc0yqsol  48613  itschlc0xyqsol1  48615  aacllem  49031