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  3609  eqreu  3691  sotr2  5565  sotr3  5572  sossfld  6139  ordintdif  6362  tz6.12i  6852  f1cofveqaeqALT  7199  soisoi  7269  riotaeqimp  7336  ov3  7516  tfindsg  7801  tfindsg2  7802  nnsuc  7824  findsg  7837  soseq  8099  suppssr  8135  suppssrg  8136  tfrlem9  8314  oe0lem  8438  oa00  8484  omwordi  8496  om00  8500  omass  8505  oelim2  8520  oeoa  8522  oeoe  8524  nnmwordi  8560  swoso  8666  dom2lem  8924  onsdominel  9050  f1finf1o  9174  f1finf1oOLD  9175  fiint  9235  cantnfp1lem3  9595  cantnfp1  9596  cantnflem1  9604  ttrclselem2  9641  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  10485  fpwwe2lem7  10550  fpwwe2  10556  gchdju1  10569  pwfseqlem3  10573  pwfseqlem4a  10574  pwfseqlem4  10575  gchpwdom  10583  tskss  10671  inar1  10688  gruss  10709  gruurn  10711  ltsonq  10882  distrlem4pr  10939  sqgt0sr  11019  map2psrpr  11023  letric  11234  renegcli  11443  addid0  11557  mulge0b  12013  nnge1  12174  0mnnnnn0  12434  nn0lt2  12557  zneo  12577  uzind2  12587  fzind  12592  nn0ind-raph  12594  uzwo  12830  nn01to3  12860  zbtwnre  12865  rpnnen1lem5  12900  ledivge1le  12984  xrletri  13073  qsqueeze  13121  difreicc  13405  elfzmlbp  13560  difelfznle  13563  elfzodifsumelfzo  13652  ssfzo12  13680  elfzonelfzo  13690  flflp1  13729  fleqceilz  13776  modsumfzodifsn  13869  addmodlteq  13871  om2uzf1oi  13878  expnngt1  14166  facdiv  14212  facwordi  14214  bcpasc  14246  hashdom  14304  hashgt23el  14349  hashdmpropge2  14408  ccatsymb  14507  swrdnnn0nd  14581  swrdnd0  14582  swrdsbslen  14589  swrdspsleq  14590  swrdlsw  14592  pfxnd0  14613  swrdswrdlem  14628  swrdccatin1  14649  pfxccatin12lem3  14656  swrdccat  14659  pfxccat3a  14662  repswswrd  14708  cshwidx0  14730  cshwcsh2id  14753  limsupbnd1  15407  lo1bdd2  15449  addcn2  15519  mulcn2  15521  o1rlimmul  15544  lo1add  15552  lo1mul  15553  rlimno1  15579  ruclem3  16160  odd2np1  16270  oddge22np1  16278  bitsfzo  16364  cncongr1  16596  2mulprm  16622  prm23ge5  16745  pcdvdsb  16799  pcaddlem  16818  infpnlem1  16840  prmunb  16844  vdwlem9  16919  vdwnnlem3  16927  ramcl  16959  prmgaplem5  16985  cshwshash  17034  setcmon  18012  setcepi  18013  setciso  18016  xpsmnd0  18670  f1ghm0to0  19142  ghmf1  19143  sylow2alem2  19515  sylow2blem3  19519  qusabl  19762  lt6abl  19792  cyggexb  19796  gsumcom2  19872  ringurd  20088  imasring  20233  xpsring1d  20236  0ring1eq0  20436  subrgdvds  20489  rngciso  20541  ringciso  20575  isdomn4  20619  drnginvrcl  20656  drnginvrl  20659  drnginvrr  20660  lsmelval2  21007  quscrng  21208  xrsdsreclblem  21337  obs2ss  21654  obslbs  21655  rnasclassa  21820  mplsubrglem  21929  psdmul  22069  gsummoncoe1  22211  mp2pm2mplem4  22712  chfacfisf  22757  chfacfisfcpmat  22758  cayleyhamilton1  22795  cmpsublem  23302  cmpsub  23303  1stccnp  23365  locfincf  23434  txhaus  23550  xkohaus  23556  ufilss  23808  cfinufil  23831  fmfnfmlem1  23857  hausflim  23884  fclscf  23928  alexsubb  23949  qustgplem  24024  prdsbl  24395  metss2lem  24415  nghmcn  24649  cfil3i  25185  cmetcaulem  25204  minveclem4  25348  ovolgelb  25397  ovolunnul  25417  ovoliun  25422  ovoliunnul  25424  ovolicc2lem2  25435  iundisj2  25466  voliunlem3  25469  rolle  25910  dvlip  25914  lhop1lem  25934  lhop2  25936  dvfsumrlim  25954  deg1ge  26019  coeeulem  26145  dgrco  26197  radcnvlt1  26343  psercnlem1  26351  logcnlem2  26568  logcnlem3  26569  cxpeq  26683  angpined  26756  efrlim  26895  efrlimOLD  26896  dmgmaddn0  26949  lgamucov  26964  basellem2  27008  ppieq0  27102  mumullem2  27106  chpeq0  27135  chteq0  27136  chtub  27139  fsumvma  27140  dchrptlem1  27191  bposlem6  27216  gausslemma2dlem0i  27291  gausslemma2dlem1a  27292  lgseisenlem2  27303  2sqlem6  27350  2sq2  27360  2sqnn0  27365  2sqreulem1  27373  2sqreunnlem1  27376  dchrisum0lem1  27443  pntrsumbnd2  27494  pntlem3  27536  noextenddif  27596  nosupno  27631  nosupbnd1  27642  noinfno  27646  noinfbnd1  27657  noetasuplem4  27664  noetainflem4  27668  scutun12  27739  slerec  27748  cutlt  27863  sleadd2im  27918  onsiso  28192  n0sfincut  28269  colinearalg  28873  eengtrkg  28949  incistruhgr  29042  wlkv0  29613  crctcshwlkn0  29784  clwwlkccatlem  29951  clwlkclwwlklem2a4  29959  clwlkclwwlklem2  29962  clwlkclwwlkfo  29971  eucrctshift  30205  frrusgrord0  30302  frgrreg  30356  blocni  30767  ubthlem1  30832  minvecolem4  30842  shmodsi  31351  atcvati  32348  atcvat2i  32349  chirredlem4  32355  atmd2  32362  sumdmdlem  32380  addltmulALT  32408  iundisj2f  32552  iundisj2fi  32753  f1resveqaeq  35051  erdszelem9  35171  satffunlem1lem2  35375  satffunlem2lem2  35378  rdgprc  35767  cgrsub  36018  btwnxfr  36029  lineext  36049  linecgr  36054  btwnconn1lem4  36063  btwnconn1lem5  36064  btwnconn1lem6  36065  btwnconn1lem8  36067  btwnconn1lem11  36070  mptsnunlem  37311  finxpreclem6  37369  ltflcei  37587  poimirlem23  37622  poimirlem24  37623  poimirlem31  37630  poimirlem32  37631  ftc1anclem5  37676  heiborlem6  37795  grpokerinj  37872  dvrunz  37933  isdmn3  38053  dmncan1  38055  membpartlem19  38788  l1cvpat  39032  atnle  39295  cvlexch3  39310  cvlexch4N  39311  cvlatexchb1  39312  cvrat2  39408  atlelt  39417  3dimlem4a  39442  3dimlem4OLDN  39444  ps-1  39456  ps-2  39457  4atlem10  39585  4atlem11  39588  4atlem12  39591  cdleme11c  40240  cdleme21c  40306  cdlemg6d  40600  trlcoat  40702  tendoid0  40804  cdleml3N  40957  dia2dimlem7  41049  aks6d1c6lem3  42145  expeq1d  42297  fsuppind  42563  pellexlem1  42802  pellexlem6  42807  imasgim  43073  onsupmaxb  43212  safesnsupfidom1o  43390  reabsifnpos  43606  reabsifnneg  43608  iunrelexpmin1  43681  iunrelexpmin2  43685  radcnvrat  44287  nzss  44290  pwclaxpow  44958  ormkglobd  46857  elprneb  47014  or2expropbi  47019  tz6.12i-afv2  47228  dfatcolem  47240  f1oresf1o2  47276  zm1nn  47287  2ffzoeq  47312  modmkpkne  47346  sfprmdvdsmersenne  47588  lighneallem3  47592  lighneallem4  47595  requad01  47606  fppr2odd  47716  fpprwppr  47724  stgoldbwt  47761  sbgoldbaltlem1  47764  isuspgrimlem  47879  upgrimpthslem2  47892  isubgr3stgrlem4  47952  isubgr3stgrlem7  47955  gpg5nbgrvtx03starlem1  48043  gpg5nbgrvtx03starlem3  48045  gpg5nbgrvtx13starlem1  48046  gpg5nbgrvtx13starlem3  48048  lmod0rng  48201  lidldomn1  48203  rngcisoALTV  48249  ringcisoALTV  48283  ztprmneprm  48319  lincresunit3  48454  itsclc0yqsol  48737  itschlc0xyqsol1  48739  aacllem  49774