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  2957  sotr2  4343  ordtr3  4437  ordintdif  4441  tfindsg  4651  tfindsg2  4652  nnsuc  4673  findsg  4683  sossfld  5120  tz6.12i  5548  suppssr  5659  soisoi  5825  ov3  5984  tfrlem9  6401  oe0lem  6512  oa00  6557  omwordi  6569  om00  6573  omass  6578  oelim2  6593  oeoa  6595  oeoe  6597  nnmwordi  6633  swoso  6691  dom2lem  6901  onsdominel  7010  f1finf1o  7086  cantnfp1lem3  7382  cantnfp1  7383  cantnflem1  7391  rankr1ai  7470  rankval3b  7498  harcard  7611  infxpenlem  7641  alephnbtwn  7698  alephinit  7722  infxp  7841  cofsmo  7895  infpssALT  7939  fin23lem24  7948  fin56  8019  ttukeylem6  8141  ficard  8187  alephval2  8194  fpwwe2lem8  8259  fpwwe2  8265  gchcda1  8278  pwfseqlem3  8282  pwfseqlem4a  8283  pwfseqlem4  8284  gchpwdom  8296  tskss  8380  inar1  8397  gruss  8418  gruurn  8420  ltsonq  8593  distrlem4pr  8650  sqgt0sr  8728  map2psrpr  8732  letric  8921  renegcli  9108  nnge1  9772  zneo  10094  uzind2  10104  fzind  10110  nn0ind-raph  10112  uzwo  10281  uzwoOLD  10282  zbtwnre  10314  rpnnen1lem5  10346  xrletri  10485  qsqueeze  10528  difreicc  10767  om2uzf1oi  11016  facdiv  11300  facwordi  11302  bcpasc  11333  hashdom  11361  limsupbnd1  11956  lo1bdd2  11998  addcn2  12067  mulcn2  12069  o1rlimmul  12092  lo1add  12100  lo1mul  12101  rlimno1  12127  znnenlem  12490  ruclem3  12511  odd2np1  12587  bitsfzo  12626  pcdvdsb  12921  pcaddlem  12936  infpnlem1  12957  prmunb  12961  vdwlem9  13036  vdwnnlem3  13044  ramcl  13076  setcmon  13919  setcepi  13920  setciso  13923  ghmf1  14711  sylow2alem2  14929  sylow2blem3  14933  divsabl  15157  lt6abl  15181  cyggexb  15185  gsumcom2  15226  imasrng  15402  drnginvrcl  15529  drnginvrl  15531  drnginvrr  15532  subrgdvds  15559  lsmelval2  15838  divscrng  15992  mplsubrglem  16183  xrsdsreclblem  16417  obs2ss  16629  obslbs  16630  cmpsublem  17126  cmpsub  17127  1stccnp  17188  txhaus  17341  xkohaus  17347  ufilss  17600  cfinufil  17623  fmfnfmlem1  17649  hausflim  17676  fclscf  17720  alexsubb  17740  divstgplem  17803  prdsbl  18037  metss2lem  18057  nghmcn  18254  cfil3i  18695  cmetcaulem  18714  minveclem4  18796  ovolgelb  18839  ovolunnul  18859  ovoliun  18864  ovoliunnul  18866  ovolicc2lem2  18877  iundisj2  18906  voliunlem3  18909  rolle  19337  dvlip  19340  lhop1lem  19360  lhop2  19362  dvfsumrlim  19378  deg1ge  19484  coeeulem  19606  dgrco  19656  radcnvlt1  19794  psercnlem1  19801  logcnlem2  19990  logcnlem3  19991  cxpeq  20097  angpined  20127  efrlim  20264  basellem2  20319  ppieq0  20414  mumullem2  20418  chpeq0  20447  chteq0  20448  chtub  20451  fsumvma  20452  dchrptlem1  20503  bposlem6  20528  lgseisenlem2  20589  2sqlem6  20608  dchrisum0lem1  20665  pntrsumbnd2  20716  pntlem3  20758  dvrunz  21100  blocni  21383  ubthlem1  21449  minvecolem4  21459  shmodsi  21968  atcvati  22966  atcvat2i  22967  chirredlem4  22973  atmd2  22980  sumdmdlem  22998  addltmulALT  23026  iundisj2fi  23364  iundisj2f  23366  dmgmaddn0  23695  erdszelem9  23730  mulge0b  24086  rdgprc  24151  soseq  24254  colinearalg  24538  cgrsub  24668  btwnxfr  24679  lineext  24699  linecgr  24704  btwnconn1lem4  24713  btwnconn1lem5  24714  btwnconn1lem6  24715  btwnconn1lem8  24717  btwnconn1lem11  24720  iintlem1  25610  intvconlem1  25703  dualcat2  25784  locfincf  26306  heiborlem6  26540  grpokerinj  26575  isdmn3  26699  dmncan1  26701  pellexlem1  26914  pellexlem6  26919  imasgim  27264  l1cvpat  29244  atnle  29507  cvlexch3  29522  cvlexch4N  29523  cvlatexchb1  29524  cvrat2  29618  atlelt  29627  3dimlem4a  29652  3dimlem4OLDN  29654  ps-1  29666  ps-2  29667  4atlem10  29795  4atlem11  29798  4atlem12  29801  cdleme11c  30450  cdleme21c  30516  cdlemg6d  30810  trlcoat  30912  tendoid0  31014  cdleml3N  31167  dia2dimlem7  31260
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