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  3033  sotr2  4422  ordtr3  4516  ordintdif  4520  tfindsg  4730  tfindsg2  4731  nnsuc  4752  findsg  4762  sossfld  5199  tz6.12i  5628  suppssr  5739  soisoi  5909  ov3  6068  tfrlem9  6485  oe0lem  6596  oa00  6641  omwordi  6653  om00  6657  omass  6662  oelim2  6677  oeoa  6679  oeoe  6681  nnmwordi  6717  swoso  6775  dom2lem  6986  onsdominel  7095  f1finf1o  7173  cantnfp1lem3  7469  cantnfp1  7470  cantnflem1  7478  rankr1ai  7557  rankval3b  7585  harcard  7698  infxpenlem  7728  alephnbtwn  7785  alephinit  7809  infxp  7928  cofsmo  7982  infpssALT  8026  fin23lem24  8035  fin56  8106  ttukeylem6  8228  ficard  8274  alephval2  8281  fpwwe2lem8  8346  fpwwe2  8352  gchcda1  8365  pwfseqlem3  8369  pwfseqlem4a  8370  pwfseqlem4  8371  gchpwdom  8383  tskss  8467  inar1  8484  gruss  8505  gruurn  8507  ltsonq  8680  distrlem4pr  8737  sqgt0sr  8815  map2psrpr  8819  letric  9008  renegcli  9195  nnge1  9859  zneo  10183  uzind2  10193  fzind  10199  nn0ind-raph  10201  uzwo  10370  uzwoOLD  10371  zbtwnre  10403  rpnnen1lem5  10435  xrletri  10574  qsqueeze  10617  difreicc  10856  om2uzf1oi  11105  facdiv  11390  facwordi  11392  bcpasc  11423  hashdom  11451  limsupbnd1  12046  lo1bdd2  12088  addcn2  12157  mulcn2  12159  o1rlimmul  12182  lo1add  12190  lo1mul  12191  rlimno1  12217  znnenlem  12581  ruclem3  12602  odd2np1  12678  bitsfzo  12717  pcdvdsb  13012  pcaddlem  13027  infpnlem1  13048  prmunb  13052  vdwlem9  13127  vdwnnlem3  13135  ramcl  13167  setcmon  14012  setcepi  14013  setciso  14016  ghmf1  14804  sylow2alem2  15022  sylow2blem3  15026  divsabl  15250  lt6abl  15274  cyggexb  15278  gsumcom2  15319  imasrng  15495  drnginvrcl  15622  drnginvrl  15624  drnginvrr  15625  subrgdvds  15652  lsmelval2  15931  divscrng  16085  mplsubrglem  16276  xrsdsreclblem  16517  obs2ss  16729  obslbs  16730  cmpsublem  17226  cmpsub  17227  1stccnp  17288  txhaus  17441  xkohaus  17447  ufilss  17696  cfinufil  17719  fmfnfmlem1  17745  hausflim  17772  fclscf  17816  alexsubb  17836  divstgplem  17899  prdsbl  18133  metss2lem  18153  nghmcn  18350  cfil3i  18793  cmetcaulem  18812  minveclem4  18894  ovolgelb  18937  ovolunnul  18957  ovoliun  18962  ovoliunnul  18964  ovolicc2lem2  18975  iundisj2  19004  voliunlem3  19007  rolle  19435  dvlip  19438  lhop1lem  19458  lhop2  19460  dvfsumrlim  19476  deg1ge  19582  coeeulem  19704  dgrco  19754  radcnvlt1  19895  psercnlem1  19902  logcnlem2  20095  logcnlem3  20096  cxpeq  20202  angpined  20232  efrlim  20369  basellem2  20425  ppieq0  20520  mumullem2  20524  chpeq0  20553  chteq0  20554  chtub  20557  fsumvma  20558  dchrptlem1  20609  bposlem6  20634  lgseisenlem2  20695  2sqlem6  20714  dchrisum0lem1  20771  pntrsumbnd2  20822  pntlem3  20864  dvrunz  21206  blocni  21491  ubthlem1  21557  minvecolem4  21567  shmodsi  22076  atcvati  23074  atcvat2i  23075  chirredlem4  23081  atmd2  23088  sumdmdlem  23106  addltmulALT  23134  iundisj2f  23225  iundisj2fi  23354  kerf1hrm  23428  dmgmaddn0  24056  lgamucov  24071  erdszelem9  24134  mulge0b  24492  rdgprc  24709  soseq  24812  colinearalg  25097  cgrsub  25227  btwnxfr  25238  lineext  25258  linecgr  25263  btwnconn1lem4  25272  btwnconn1lem5  25273  btwnconn1lem6  25274  btwnconn1lem8  25276  btwnconn1lem11  25279  ltflcei  25485  lxflflp1  25487  itg2addnc  25494  locfincf  25630  heiborlem6  25863  grpokerinj  25898  isdmn3  26022  dmncan1  26024  pellexlem1  26237  pellexlem6  26242  imasgim  26587  hashle00  27483  l1cvpat  29296  atnle  29559  cvlexch3  29574  cvlexch4N  29575  cvlatexchb1  29576  cvrat2  29670  atlelt  29679  3dimlem4a  29704  3dimlem4OLDN  29706  ps-1  29718  ps-2  29719  4atlem10  29847  4atlem11  29850  4atlem12  29853  cdleme11c  30502  cdleme21c  30568  cdlemg6d  30862  trlcoat  30964  tendoid0  31066  cdleml3N  31219  dia2dimlem7  31312
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