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  3085  eqreu  3146  sotr2  4665  ordtr3  4759  ordintdif  4763  sossfld  5280  tz6.12i  5705  suppssrOLD  5832  soisoi  6014  ov3  6222  tfindsg  6466  tfindsg2  6467  nnsuc  6488  findsg  6498  suppssr  6715  tfrlem9  6836  oe0lem  6945  oa00  6990  omwordi  7002  om00  7006  omass  7011  oelim2  7026  oeoa  7028  oeoe  7030  nnmwordi  7066  swoso  7124  dom2lem  7341  onsdominel  7452  f1finf1o  7531  cantnfp1lem3  7880  cantnfp1  7881  cantnflem1  7889  cantnfp1lem3OLD  7906  cantnfp1OLD  7907  cantnflem1OLD  7912  rankr1ai  7997  rankval3b  8025  harcard  8140  infxpenlem  8172  alephnbtwn  8233  alephinit  8257  infxp  8376  cofsmo  8430  infpssALT  8474  fin23lem24  8483  fin56  8554  ttukeylem6  8675  ficard  8721  alephval2  8728  fpwwe2lem8  8796  fpwwe2  8802  gchcda1  8815  pwfseqlem3  8819  pwfseqlem4a  8820  pwfseqlem4  8821  gchpwdom  8829  tskss  8917  inar1  8934  gruss  8955  gruurn  8957  ltsonq  9130  distrlem4pr  9187  sqgt0sr  9265  map2psrpr  9269  letric  9467  renegcli  9662  mulge0b  10191  nnge1  10340  0mnnnnn0  10604  zneo  10716  uzind2  10726  fzind  10732  nn0ind-raph  10734  uzwo  10909  uzwoOLD  10910  zbtwnre  10943  rpnnen1lem5  10975  xrletri  11120  qsqueeze  11163  difreicc  11409  elfzmlbp  11483  elfzodifsumelfzo  11596  ssfzo12  11612  elfzonelfzo  11619  fleqceilz  11685  om2uzf1oi  11768  facdiv  12055  facwordi  12057  bcpasc  12089  hashdom  12134  hashle00  12150  lswcl  12262  ccatsymb  12273  ccatval1lsw  12275  swrdspsleq  12334  swrdlsw  12338  swrdswrdlem  12345  swrdccatin1  12366  swrdccatin12lem3  12373  repswswrd  12414  cshwidx0  12434  limsupbnd1  12952  lo1bdd2  12994  addcn2  13063  mulcn2  13065  o1rlimmul  13088  lo1add  13096  lo1mul  13097  rlimno1  13123  znnenlem  13486  ruclem3  13507  odd2np1  13584  bitsfzo  13623  pcdvdsb  13927  pcaddlem  13942  infpnlem1  13963  prmunb  13967  vdwlem9  14042  vdwnnlem3  14050  ramcl  14082  cshwshash  14123  setcmon  14947  setcepi  14948  setciso  14951  ghmf1  15766  sylow2alem2  16108  sylow2blem3  16112  divsabl  16338  lt6abl  16362  cyggexb  16366  gsumcom2  16457  imasrng  16701  drnginvrcl  16829  drnginvrl  16831  drnginvrr  16832  subrgdvds  16859  lsmelval2  17146  divscrng  17302  mplsubrglem  17497  mplsubrglemOLD  17498  xrsdsreclblem  17839  obs2ss  18134  obslbs  18135  cmpsublem  18982  cmpsub  18983  1stccnp  19046  txhaus  19200  xkohaus  19206  ufilss  19458  cfinufil  19481  fmfnfmlem1  19507  hausflim  19534  fclscf  19578  alexsubb  19598  divstgplem  19671  prdsbl  20046  metss2lem  20066  nghmcn  20304  cfil3i  20760  cmetcaulem  20779  minveclem4  20899  ovolgelb  20943  ovolunnul  20963  ovoliun  20968  ovoliunnul  20970  ovolicc2lem2  20981  iundisj2  21010  voliunlem3  21013  rolle  21442  dvlip  21445  lhop1lem  21465  lhop2  21467  dvfsumrlim  21483  deg1ge  21550  coeeulem  21672  dgrco  21722  radcnvlt1  21863  psercnlem1  21870  logcnlem2  22068  logcnlem3  22069  cxpeq  22175  angpined  22205  efrlim  22343  basellem2  22399  ppieq0  22494  mumullem2  22498  chpeq0  22527  chteq0  22528  chtub  22531  fsumvma  22532  dchrptlem1  22583  bposlem6  22608  lgseisenlem2  22669  2sqlem6  22688  dchrisum0lem1  22745  pntrsumbnd2  22796  pntlem3  22838  colinearalg  23124  eengtrkg  23199  dvrunz  23888  blocni  24173  ubthlem1  24239  minvecolem4  24249  shmodsi  24760  atcvati  25758  atcvat2i  25759  chirredlem4  25765  atmd2  25772  sumdmdlem  25790  addltmulALT  25818  iundisj2f  25900  iundisj2fi  26049  kerf1hrm  26260  dmgmaddn0  26978  lgamucov  26993  erdszelem9  27056  rdgprc  27577  soseq  27684  cgrsub  28045  btwnxfr  28056  lineext  28076  linecgr  28081  btwnconn1lem4  28090  btwnconn1lem5  28091  btwnconn1lem6  28092  btwnconn1lem8  28094  btwnconn1lem11  28097  ltflcei  28390  lxflflp1  28392  ftc1anclem5  28442  locfincf  28549  heiborlem6  28686  grpokerinj  28721  isdmn3  28845  dmncan1  28847  pellexlem1  29141  pellexlem6  29146  imasgim  29426  lesubnn0  30152  nn0lt2  30157  nn01to3  30158  2ffzoeq  30185  elfzom1elp1fzo  30189  prmn2uzge3  30220  wlkv0  30262  usgra2pthspth  30266  0clwlk  30399  clwwlkgt0  30405  clwlkisclwwlklem2a4  30417  clwlkisclwwlklem1  30420  zm1nn  30439  erclwwlktr0  30450  difelfznle  30459  nbhashuvtx1  30504  ztprmneprm  30709  lmod0rng  30748  gsummoncoe1  30808  lincresunit3  30946  l1cvpat  32592  atnle  32855  cvlexch3  32870  cvlexch4N  32871  cvlatexchb1  32872  cvrat2  32966  atlelt  32975  3dimlem4a  33000  3dimlem4OLDN  33002  ps-1  33014  ps-2  33015  4atlem10  33143  4atlem11  33146  4atlem12  33149  cdleme11c  33798  cdleme21c  33864  cdlemg6d  34158  trlcoat  34260  tendoid0  34362  cdleml3N  34515  dia2dimlem7  34608
  Copyright terms: Public domain W3C validator