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

Theorem sylbird 227
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 215 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbird.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 42 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr3d  259  eqreu  3094  sotr2  4500  ordtr3  4594  ordintdif  4598  tfindsg  4807  tfindsg2  4808  nnsuc  4829  findsg  4839  sossfld  5284  tz6.12i  5718  suppssr  5831  soisoi  6015  ov3  6177  tfrlem9  6613  oe0lem  6724  oa00  6769  omwordi  6781  om00  6785  omass  6790  oelim2  6805  oeoa  6807  oeoe  6809  nnmwordi  6845  swoso  6903  dom2lem  7114  onsdominel  7223  f1finf1o  7302  cantnfp1lem3  7600  cantnfp1  7601  cantnflem1  7609  rankr1ai  7688  rankval3b  7716  harcard  7829  infxpenlem  7859  alephnbtwn  7916  alephinit  7940  infxp  8059  cofsmo  8113  infpssALT  8157  fin23lem24  8166  fin56  8237  ttukeylem6  8358  ficard  8404  alephval2  8411  fpwwe2lem8  8476  fpwwe2  8482  gchcda1  8495  pwfseqlem3  8499  pwfseqlem4a  8500  pwfseqlem4  8501  gchpwdom  8513  tskss  8597  inar1  8614  gruss  8635  gruurn  8637  ltsonq  8810  distrlem4pr  8867  sqgt0sr  8945  map2psrpr  8949  letric  9138  renegcli  9326  nnge1  9990  zneo  10316  uzind2  10326  fzind  10332  nn0ind-raph  10334  uzwo  10503  uzwoOLD  10504  zbtwnre  10536  rpnnen1lem5  10568  xrletri  10708  qsqueeze  10751  difreicc  10992  om2uzf1oi  11256  facdiv  11541  facwordi  11543  bcpasc  11575  hashdom  11616  hashle00  11632  limsupbnd1  12239  lo1bdd2  12281  addcn2  12350  mulcn2  12352  o1rlimmul  12375  lo1add  12383  lo1mul  12384  rlimno1  12410  znnenlem  12774  ruclem3  12795  odd2np1  12871  bitsfzo  12910  pcdvdsb  13205  pcaddlem  13220  infpnlem1  13241  prmunb  13245  vdwlem9  13320  vdwnnlem3  13328  ramcl  13360  setcmon  14205  setcepi  14206  setciso  14209  ghmf1  14997  sylow2alem2  15215  sylow2blem3  15219  divsabl  15443  lt6abl  15467  cyggexb  15471  gsumcom2  15512  imasrng  15688  drnginvrcl  15815  drnginvrl  15817  drnginvrr  15818  subrgdvds  15845  lsmelval2  16120  divscrng  16274  mplsubrglem  16465  xrsdsreclblem  16707  obs2ss  16919  obslbs  16920  cmpsublem  17424  cmpsub  17425  1stccnp  17486  txhaus  17640  xkohaus  17646  ufilss  17898  cfinufil  17921  fmfnfmlem1  17947  hausflim  17974  fclscf  18018  alexsubb  18038  divstgplem  18111  prdsbl  18482  metss2lem  18502  nghmcn  18740  cfil3i  19183  cmetcaulem  19202  minveclem4  19294  ovolgelb  19337  ovolunnul  19357  ovoliun  19362  ovoliunnul  19364  ovolicc2lem2  19375  iundisj2  19404  voliunlem3  19407  rolle  19835  dvlip  19838  lhop1lem  19858  lhop2  19860  dvfsumrlim  19876  deg1ge  19982  coeeulem  20104  dgrco  20154  radcnvlt1  20295  psercnlem1  20302  logcnlem2  20495  logcnlem3  20496  cxpeq  20602  angpined  20632  efrlim  20769  basellem2  20825  ppieq0  20920  mumullem2  20924  chpeq0  20953  chteq0  20954  chtub  20957  fsumvma  20958  dchrptlem1  21009  bposlem6  21034  lgseisenlem2  21095  2sqlem6  21114  dchrisum0lem1  21171  pntrsumbnd2  21222  pntlem3  21264  dvrunz  21982  blocni  22267  ubthlem1  22333  minvecolem4  22343  shmodsi  22852  atcvati  23850  atcvat2i  23851  chirredlem4  23857  atmd2  23864  sumdmdlem  23882  addltmulALT  23910  iundisj2f  23991  iundisj2fi  24114  kerf1hrm  24223  dmgmaddn0  24768  lgamucov  24783  erdszelem9  24846  mulge0b  25152  rdgprc  25373  soseq  25476  colinearalg  25761  cgrsub  25891  btwnxfr  25902  lineext  25922  linecgr  25927  btwnconn1lem4  25936  btwnconn1lem5  25937  btwnconn1lem6  25938  btwnconn1lem8  25940  btwnconn1lem11  25943  ltflcei  26148  lxflflp1  26150  locfincf  26284  heiborlem6  26423  grpokerinj  26458  isdmn3  26582  dmncan1  26584  pellexlem1  26790  pellexlem6  26795  imasgim  27140  0mnnnnn0  27979  lesubnn0  27980  elfzmlbp  27986  ssfzo12  27998  elfzonelfzo  28000  swrdswrdlem  28018  swrdccatin1  28024  swrdccatin12lem3  28032  swrdccatin12c  28036  swrdccat3  28037  usgra2pthspth  28043  l1cvpat  29549  atnle  29812  cvlexch3  29827  cvlexch4N  29828  cvlatexchb1  29829  cvrat2  29923  atlelt  29932  3dimlem4a  29957  3dimlem4OLDN  29959  ps-1  29971  ps-2  29972  4atlem10  30100  4atlem11  30103  4atlem12  30106  cdleme11c  30755  cdleme21c  30821  cdlemg6d  31115  trlcoat  31217  tendoid0  31319  cdleml3N  31472  dia2dimlem7  31565
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 178
  Copyright terms: Public domain W3C validator