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

Theorem sylbird 226
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 214 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbird.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 40 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr3d  258  eqreu  2970  sotr2  4359  ordtr3  4453  ordintdif  4457  tfindsg  4667  tfindsg2  4668  nnsuc  4689  findsg  4699  sossfld  5136  tz6.12i  5564  suppssr  5675  soisoi  5841  ov3  6000  tfrlem9  6417  oe0lem  6528  oa00  6573  omwordi  6585  om00  6589  omass  6594  oelim2  6609  oeoa  6611  oeoe  6613  nnmwordi  6649  swoso  6707  dom2lem  6917  onsdominel  7026  f1finf1o  7102  cantnfp1lem3  7398  cantnfp1  7399  cantnflem1  7407  rankr1ai  7486  rankval3b  7514  harcard  7627  infxpenlem  7657  alephnbtwn  7714  alephinit  7738  infxp  7857  cofsmo  7911  infpssALT  7955  fin23lem24  7964  fin56  8035  ttukeylem6  8157  ficard  8203  alephval2  8210  fpwwe2lem8  8275  fpwwe2  8281  gchcda1  8294  pwfseqlem3  8298  pwfseqlem4a  8299  pwfseqlem4  8300  gchpwdom  8312  tskss  8396  inar1  8413  gruss  8434  gruurn  8436  ltsonq  8609  distrlem4pr  8666  sqgt0sr  8744  map2psrpr  8748  letric  8937  renegcli  9124  nnge1  9788  zneo  10110  uzind2  10120  fzind  10126  nn0ind-raph  10128  uzwo  10297  uzwoOLD  10298  zbtwnre  10330  rpnnen1lem5  10362  xrletri  10501  qsqueeze  10544  difreicc  10783  om2uzf1oi  11032  facdiv  11316  facwordi  11318  bcpasc  11349  hashdom  11377  limsupbnd1  11972  lo1bdd2  12014  addcn2  12083  mulcn2  12085  o1rlimmul  12108  lo1add  12116  lo1mul  12117  rlimno1  12143  znnenlem  12506  ruclem3  12527  odd2np1  12603  bitsfzo  12642  pcdvdsb  12937  pcaddlem  12952  infpnlem1  12973  prmunb  12977  vdwlem9  13052  vdwnnlem3  13060  ramcl  13092  setcmon  13935  setcepi  13936  setciso  13939  ghmf1  14727  sylow2alem2  14945  sylow2blem3  14949  divsabl  15173  lt6abl  15197  cyggexb  15201  gsumcom2  15242  imasrng  15418  drnginvrcl  15545  drnginvrl  15547  drnginvrr  15548  subrgdvds  15575  lsmelval2  15854  divscrng  16008  mplsubrglem  16199  xrsdsreclblem  16433  obs2ss  16645  obslbs  16646  cmpsublem  17142  cmpsub  17143  1stccnp  17204  txhaus  17357  xkohaus  17363  ufilss  17616  cfinufil  17639  fmfnfmlem1  17665  hausflim  17692  fclscf  17736  alexsubb  17756  divstgplem  17819  prdsbl  18053  metss2lem  18073  nghmcn  18270  cfil3i  18711  cmetcaulem  18730  minveclem4  18812  ovolgelb  18855  ovolunnul  18875  ovoliun  18880  ovoliunnul  18882  ovolicc2lem2  18893  iundisj2  18922  voliunlem3  18925  rolle  19353  dvlip  19356  lhop1lem  19376  lhop2  19378  dvfsumrlim  19394  deg1ge  19500  coeeulem  19622  dgrco  19672  radcnvlt1  19810  psercnlem1  19817  logcnlem2  20006  logcnlem3  20007  cxpeq  20113  angpined  20143  efrlim  20280  basellem2  20335  ppieq0  20430  mumullem2  20434  chpeq0  20463  chteq0  20464  chtub  20467  fsumvma  20468  dchrptlem1  20519  bposlem6  20544  lgseisenlem2  20605  2sqlem6  20624  dchrisum0lem1  20681  pntrsumbnd2  20732  pntlem3  20774  dvrunz  21116  blocni  21399  ubthlem1  21465  minvecolem4  21475  shmodsi  21984  atcvati  22982  atcvat2i  22983  chirredlem4  22989  atmd2  22996  sumdmdlem  23014  addltmulALT  23042  iundisj2fi  23379  iundisj2f  23381  dmgmaddn0  23710  erdszelem9  23745  mulge0b  24101  rdgprc  24222  soseq  24325  colinearalg  24610  cgrsub  24740  btwnxfr  24751  lineext  24771  linecgr  24776  btwnconn1lem4  24785  btwnconn1lem5  24786  btwnconn1lem6  24787  btwnconn1lem8  24789  btwnconn1lem11  24792  ltflcei  24998  lxflflp1  25000  itg2addnc  25005  iintlem1  25713  intvconlem1  25806  dualcat2  25887  locfincf  26409  heiborlem6  26643  grpokerinj  26678  isdmn3  26802  dmncan1  26804  pellexlem1  27017  pellexlem6  27022  imasgim  27367  l1cvpat  29866  atnle  30129  cvlexch3  30144  cvlexch4N  30145  cvlatexchb1  30146  cvrat2  30240  atlelt  30249  3dimlem4a  30274  3dimlem4OLDN  30276  ps-1  30288  ps-2  30289  4atlem10  30417  4atlem11  30420  4atlem12  30423  cdleme11c  31072  cdleme21c  31138  cdlemg6d  31432  trlcoat  31534  tendoid0  31636  cdleml3N  31789  dia2dimlem7  31882
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator