MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbird Structured version   Unicode version

Theorem sylbird 235
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbird.1  |-  ( ph  ->  ( ch  <->  ps )
)
sylbird.2  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
sylbird  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem sylbird
StepHypRef Expression
1 sylbird.1 . . 3  |-  ( ph  ->  ( ch  <->  ps )
)
21biimprd 223 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbird.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 44 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3imtr3d  267  ceqex  3230  eqreu  3291  sotr2  4838  ordtr3  4932  ordintdif  4936  sossfld  5460  tz6.12i  5892  suppssrOLD  6022  soisoi  6225  ov3  6438  tfindsg  6694  tfindsg2  6695  nnsuc  6716  findsg  6726  suppssr  6949  tfrlem9  7072  oe0lem  7181  oa00  7226  omwordi  7238  om00  7242  omass  7247  oelim2  7262  oeoa  7264  oeoe  7266  nnmwordi  7302  swoso  7360  dom2lem  7574  onsdominel  7685  f1finf1o  7765  cantnfp1lem3  8116  cantnfp1  8117  cantnflem1  8125  cantnfp1lem3OLD  8142  cantnfp1OLD  8143  cantnflem1OLD  8148  rankr1ai  8233  rankval3b  8261  harcard  8376  infxpenlem  8408  alephnbtwn  8469  alephinit  8493  infxp  8612  cofsmo  8666  infpssALT  8710  fin23lem24  8719  fin56  8790  ttukeylem6  8911  ficard  8957  alephval2  8964  fpwwe2lem8  9032  fpwwe2  9038  gchcda1  9051  pwfseqlem3  9055  pwfseqlem4a  9056  pwfseqlem4  9057  gchpwdom  9065  tskss  9153  inar1  9170  gruss  9191  gruurn  9193  ltsonq  9364  distrlem4pr  9421  sqgt0sr  9500  map2psrpr  9504  letric  9702  renegcli  9899  mulge0b  10433  nnge1  10582  0mnnnnn0  10849  nn0lt2  10948  zneo  10966  uzind2  10976  fzind  10983  nn0ind-raph  10985  uzwo  11169  uzwoOLD  11170  nn01to3  11200  zbtwnre  11205  rpnnen1lem5  11237  xrletri  11382  qsqueeze  11425  difreicc  11677  elfzmlbp  11812  difelfznle  11815  elfzodifsumelfzo  11885  ssfzo12  11908  elfzonelfzo  11915  flflp1  11947  fleqceilz  11984  om2uzf1oi  12067  facdiv  12368  facwordi  12370  bcpasc  12402  hashdom  12450  hashle00  12469  ccatsymb  12609  swrdsbslen  12685  swrdspsleq  12686  swrdlsw  12689  swrdswrdlem  12696  swrdccatin1  12720  swrdccatin12lem3  12727  repswswrd  12768  cshwidx0  12788  cshwcsh2id  12808  limsupbnd1  13317  lo1bdd2  13359  addcn2  13428  mulcn2  13430  o1rlimmul  13453  lo1add  13461  lo1mul  13462  rlimno1  13488  znnenlem  13957  ruclem3  13978  odd2np1  14058  bitsfzo  14097  prmn2uzge3  14249  pcdvdsb  14404  pcaddlem  14419  infpnlem1  14440  prmunb  14444  vdwlem9  14519  vdwnnlem3  14527  ramcl  14559  cshwshash  14601  setcmon  15493  setcepi  15494  setciso  15497  ghmf1  16422  sylow2alem2  16765  sylow2blem3  16769  qusabl  16998  lt6abl  17024  cyggexb  17028  gsumcom2  17130  imasring  17395  f1rhm0to0  17516  drnginvrcl  17540  drnginvrl  17542  drnginvrr  17543  subrgdvds  17570  lsmelval2  17858  quscrng  18015  mplsubrglem  18227  mplsubrglemOLD  18228  gsummoncoe1  18473  xrsdsreclblem  18591  obs2ss  18887  obslbs  18888  mp2pm2mplem4  19437  chfacfisf  19482  chfacfisfcpmat  19483  cayleyhamilton1  19520  cmpsublem  20026  cmpsub  20027  1stccnp  20089  locfincf  20158  txhaus  20274  xkohaus  20280  ufilss  20532  cfinufil  20555  fmfnfmlem1  20581  hausflim  20608  fclscf  20652  alexsubb  20672  qustgplem  20745  prdsbl  21120  metss2lem  21140  nghmcn  21378  cfil3i  21834  cmetcaulem  21853  minveclem4  21973  ovolgelb  22017  ovolunnul  22037  ovoliun  22042  ovoliunnul  22044  ovolicc2lem2  22055  iundisj2  22085  voliunlem3  22088  rolle  22517  dvlip  22520  lhop1lem  22540  lhop2  22542  dvfsumrlim  22558  deg1ge  22625  coeeulem  22747  dgrco  22798  radcnvlt1  22939  psercnlem1  22946  logcnlem2  23150  logcnlem3  23151  cxpeq  23257  angpined  23287  efrlim  23425  basellem2  23481  ppieq0  23576  mumullem2  23580  chpeq0  23609  chteq0  23610  chtub  23613  fsumvma  23614  dchrptlem1  23665  bposlem6  23690  lgseisenlem2  23751  2sqlem6  23770  dchrisum0lem1  23827  pntrsumbnd2  23878  pntlem3  23920  colinearalg  24340  eengtrkg  24415  wlkv0  24887  0clwlk  24892  clwwlkgt0  24898  clwlkisclwwlklem2a4  24911  clwlkisclwwlklem1  24914  nbhashuvtx1  25042  dvrunz  25562  blocni  25847  ubthlem1  25913  minvecolem4  25923  shmodsi  26434  atcvati  27432  atcvat2i  27433  chirredlem4  27439  atmd2  27446  sumdmdlem  27464  addltmulALT  27492  iundisj2f  27589  iundisj2fi  27762  rngurd  27939  dmgmaddn0  28762  lgamucov  28777  erdszelem9  28840  rdgprc  29444  soseq  29551  cgrsub  29900  btwnxfr  29911  lineext  29931  linecgr  29936  btwnconn1lem4  29945  btwnconn1lem5  29946  btwnconn1lem6  29947  btwnconn1lem8  29949  btwnconn1lem11  29952  ltflcei  30248  ftc1anclem5  30299  heiborlem6  30517  grpokerinj  30552  isdmn3  30676  dmncan1  30678  pellexlem1  30969  pellexlem6  30974  imasgim  31252  radcnvrat  31399  nzss  31426  pfxccat3a  32547  zm1nn  32589  lesubnn0  32590  2ffzoeq  32605  usgra2pthspth  32613  lmod0rng  32818  0ring1eq0  32822  lidldomn1  32871  rngciso  32934  rngcisoOLD  32946  ringciso  32985  ringcisoOLD  33009  ztprmneprm  33080  lincresunit3  33226  aacllem  33360  l1cvpat  34922  atnle  35185  cvlexch3  35200  cvlexch4N  35201  cvlatexchb1  35202  cvrat2  35296  atlelt  35305  3dimlem4a  35330  3dimlem4OLDN  35332  ps-1  35344  ps-2  35345  4atlem10  35473  4atlem11  35476  4atlem12  35479  cdleme11c  36129  cdleme21c  36196  cdlemg6d  36490  trlcoat  36592  tendoid0  36694  cdleml3N  36847  dia2dimlem7  36940
  Copyright terms: Public domain W3C validator