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  3234  eqreu  3295  sotr2  4829  ordtr3  4923  ordintdif  4927  sossfld  5454  tz6.12i  5886  suppssrOLD  6015  soisoi  6212  ov3  6423  tfindsg  6679  tfindsg2  6680  nnsuc  6701  findsg  6711  suppssr  6931  tfrlem9  7054  oe0lem  7163  oa00  7208  omwordi  7220  om00  7224  omass  7229  oelim2  7244  oeoa  7246  oeoe  7248  nnmwordi  7284  swoso  7342  dom2lem  7555  onsdominel  7666  f1finf1o  7746  cantnfp1lem3  8099  cantnfp1  8100  cantnflem1  8108  cantnfp1lem3OLD  8125  cantnfp1OLD  8126  cantnflem1OLD  8131  rankr1ai  8216  rankval3b  8244  harcard  8359  infxpenlem  8391  alephnbtwn  8452  alephinit  8476  infxp  8595  cofsmo  8649  infpssALT  8693  fin23lem24  8702  fin56  8773  ttukeylem6  8894  ficard  8940  alephval2  8947  fpwwe2lem8  9015  fpwwe2  9021  gchcda1  9034  pwfseqlem3  9038  pwfseqlem4a  9039  pwfseqlem4  9040  gchpwdom  9048  tskss  9136  inar1  9153  gruss  9174  gruurn  9176  ltsonq  9347  distrlem4pr  9404  sqgt0sr  9483  map2psrpr  9487  letric  9685  renegcli  9880  mulge0b  10412  nnge1  10562  0mnnnnn0  10828  nn0lt2  10925  zneo  10943  uzind2  10953  fzind  10959  nn0ind-raph  10961  uzwo  11144  uzwoOLD  11145  nn01to3  11175  zbtwnre  11180  rpnnen1lem5  11212  xrletri  11357  qsqueeze  11400  difreicc  11652  elfzmlbp  11783  difelfznle  11786  elfzodifsumelfzo  11850  ssfzo12  11873  elfzonelfzo  11880  flflp1  11912  fleqceilz  11949  om2uzf1oi  12032  facdiv  12333  facwordi  12335  bcpasc  12367  hashdom  12415  hashle00  12431  lswcl  12554  ccatsymb  12565  ccatval1lsw  12567  swrdspsleq  12636  swrdlsw  12640  swrdswrdlem  12647  swrdccatin1  12671  swrdccatin12lem3  12678  repswswrd  12719  cshwidx0  12739  cshwcsh2id  12759  limsupbnd1  13268  lo1bdd2  13310  addcn2  13379  mulcn2  13381  o1rlimmul  13404  lo1add  13412  lo1mul  13413  rlimno1  13439  znnenlem  13806  ruclem3  13827  odd2np1  13905  bitsfzo  13944  prmn2uzge3  14096  pcdvdsb  14251  pcaddlem  14266  infpnlem1  14287  prmunb  14291  vdwlem9  14366  vdwnnlem3  14374  ramcl  14406  cshwshash  14447  setcmon  15272  setcepi  15273  setciso  15276  ghmf1  16100  sylow2alem2  16444  sylow2blem3  16448  divsabl  16674  lt6abl  16700  cyggexb  16704  gsumcom2  16806  imasrng  17069  f1rhm0to0  17189  drnginvrcl  17213  drnginvrl  17215  drnginvrr  17216  subrgdvds  17243  lsmelval2  17531  divscrng  17687  mplsubrglem  17899  mplsubrglemOLD  17900  gsummoncoe1  18145  xrsdsreclblem  18260  obs2ss  18555  obslbs  18556  mp2pm2mplem4  19105  chfacfisf  19150  chfacfisfcpmat  19151  cayleyhamilton1  19188  cmpsublem  19693  cmpsub  19694  1stccnp  19757  txhaus  19911  xkohaus  19917  ufilss  20169  cfinufil  20192  fmfnfmlem1  20218  hausflim  20245  fclscf  20289  alexsubb  20309  divstgplem  20382  prdsbl  20757  metss2lem  20777  nghmcn  21015  cfil3i  21471  cmetcaulem  21490  minveclem4  21610  ovolgelb  21654  ovolunnul  21674  ovoliun  21679  ovoliunnul  21681  ovolicc2lem2  21692  iundisj2  21722  voliunlem3  21725  rolle  22154  dvlip  22157  lhop1lem  22177  lhop2  22179  dvfsumrlim  22195  deg1ge  22262  coeeulem  22384  dgrco  22434  radcnvlt1  22575  psercnlem1  22582  logcnlem2  22780  logcnlem3  22781  cxpeq  22887  angpined  22917  efrlim  23055  basellem2  23111  ppieq0  23206  mumullem2  23210  chpeq0  23239  chteq0  23240  chtub  23243  fsumvma  23244  dchrptlem1  23295  bposlem6  23320  lgseisenlem2  23381  2sqlem6  23400  dchrisum0lem1  23457  pntrsumbnd2  23508  pntlem3  23550  colinearalg  23917  eengtrkg  23992  wlkv0  24464  0clwlk  24469  clwwlkgt0  24475  clwlkisclwwlklem2a4  24488  clwlkisclwwlklem1  24491  nbhashuvtx1  24619  dvrunz  25139  blocni  25424  ubthlem1  25490  minvecolem4  25500  shmodsi  26011  atcvati  27009  atcvat2i  27010  chirredlem4  27016  atmd2  27023  sumdmdlem  27041  addltmulALT  27069  iundisj2f  27150  iundisj2fi  27298  dmgmaddn0  28233  lgamucov  28248  erdszelem9  28311  rdgprc  28832  soseq  28939  cgrsub  29300  btwnxfr  29311  lineext  29331  linecgr  29336  btwnconn1lem4  29345  btwnconn1lem5  29346  btwnconn1lem6  29347  btwnconn1lem8  29349  btwnconn1lem11  29352  ltflcei  29648  ftc1anclem5  29699  locfincf  29806  heiborlem6  29943  grpokerinj  29978  isdmn3  30102  dmncan1  30104  pellexlem1  30397  pellexlem6  30402  imasgim  30680  nzss  30850  zm1nn  31820  lesubnn0  31821  2ffzoeq  31836  usgra2pthspth  31846  ztprmneprm  32032  lmod0rng  32058  lincresunit3  32181  l1cvpat  33869  atnle  34132  cvlexch3  34147  cvlexch4N  34148  cvlatexchb1  34149  cvrat2  34243  atlelt  34252  3dimlem4a  34277  3dimlem4OLDN  34279  ps-1  34291  ps-2  34292  4atlem10  34420  4atlem11  34423  4atlem12  34426  cdleme11c  35075  cdleme21c  35141  cdlemg6d  35435  trlcoat  35537  tendoid0  35639  cdleml3N  35792  dia2dimlem7  35885
  Copyright terms: Public domain W3C validator