MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylbird Structured version   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  3126  sotr2  4532  ordtr3  4626  ordintdif  4630  tfindsg  4840  tfindsg2  4841  nnsuc  4862  findsg  4872  sossfld  5317  tz6.12i  5751  suppssr  5864  soisoi  6048  ov3  6210  tfrlem9  6646  oe0lem  6757  oa00  6802  omwordi  6814  om00  6818  omass  6823  oelim2  6838  oeoa  6840  oeoe  6842  nnmwordi  6878  swoso  6936  dom2lem  7147  onsdominel  7256  f1finf1o  7335  cantnfp1lem3  7636  cantnfp1  7637  cantnflem1  7645  rankr1ai  7724  rankval3b  7752  harcard  7865  infxpenlem  7895  alephnbtwn  7952  alephinit  7976  infxp  8095  cofsmo  8149  infpssALT  8193  fin23lem24  8202  fin56  8273  ttukeylem6  8394  ficard  8440  alephval2  8447  fpwwe2lem8  8512  fpwwe2  8518  gchcda1  8531  pwfseqlem3  8535  pwfseqlem4a  8536  pwfseqlem4  8537  gchpwdom  8549  tskss  8633  inar1  8650  gruss  8671  gruurn  8673  ltsonq  8846  distrlem4pr  8903  sqgt0sr  8981  map2psrpr  8985  letric  9174  renegcli  9362  nnge1  10026  zneo  10352  uzind2  10362  fzind  10368  nn0ind-raph  10370  uzwo  10539  uzwoOLD  10540  zbtwnre  10572  rpnnen1lem5  10604  xrletri  10744  qsqueeze  10787  difreicc  11028  om2uzf1oi  11293  facdiv  11578  facwordi  11580  bcpasc  11612  hashdom  11653  hashle00  11669  limsupbnd1  12276  lo1bdd2  12318  addcn2  12387  mulcn2  12389  o1rlimmul  12412  lo1add  12420  lo1mul  12421  rlimno1  12447  znnenlem  12811  ruclem3  12832  odd2np1  12908  bitsfzo  12947  pcdvdsb  13242  pcaddlem  13257  infpnlem1  13278  prmunb  13282  vdwlem9  13357  vdwnnlem3  13365  ramcl  13397  setcmon  14242  setcepi  14243  setciso  14246  ghmf1  15034  sylow2alem2  15252  sylow2blem3  15256  divsabl  15480  lt6abl  15504  cyggexb  15508  gsumcom2  15549  imasrng  15725  drnginvrcl  15852  drnginvrl  15854  drnginvrr  15855  subrgdvds  15882  lsmelval2  16157  divscrng  16311  mplsubrglem  16502  xrsdsreclblem  16744  obs2ss  16956  obslbs  16957  cmpsublem  17462  cmpsub  17463  1stccnp  17525  txhaus  17679  xkohaus  17685  ufilss  17937  cfinufil  17960  fmfnfmlem1  17986  hausflim  18013  fclscf  18057  alexsubb  18077  divstgplem  18150  prdsbl  18521  metss2lem  18541  nghmcn  18779  cfil3i  19222  cmetcaulem  19241  minveclem4  19333  ovolgelb  19376  ovolunnul  19396  ovoliun  19401  ovoliunnul  19403  ovolicc2lem2  19414  iundisj2  19443  voliunlem3  19446  rolle  19874  dvlip  19877  lhop1lem  19897  lhop2  19899  dvfsumrlim  19915  deg1ge  20021  coeeulem  20143  dgrco  20193  radcnvlt1  20334  psercnlem1  20341  logcnlem2  20534  logcnlem3  20535  cxpeq  20641  angpined  20671  efrlim  20808  basellem2  20864  ppieq0  20959  mumullem2  20963  chpeq0  20992  chteq0  20993  chtub  20996  fsumvma  20997  dchrptlem1  21048  bposlem6  21073  lgseisenlem2  21134  2sqlem6  21153  dchrisum0lem1  21210  pntrsumbnd2  21261  pntlem3  21303  dvrunz  22021  blocni  22306  ubthlem1  22372  minvecolem4  22382  shmodsi  22891  atcvati  23889  atcvat2i  23890  chirredlem4  23896  atmd2  23903  sumdmdlem  23921  addltmulALT  23949  iundisj2f  24030  iundisj2fi  24153  kerf1hrm  24262  dmgmaddn0  24807  lgamucov  24822  erdszelem9  24885  mulge0b  25191  rdgprc  25422  soseq  25529  colinearalg  25849  cgrsub  25979  btwnxfr  25990  lineext  26010  linecgr  26015  btwnconn1lem4  26024  btwnconn1lem5  26025  btwnconn1lem6  26026  btwnconn1lem8  26028  btwnconn1lem11  26031  ltflcei  26239  lxflflp1  26241  ftc1anclem5  26284  locfincf  26386  heiborlem6  26525  grpokerinj  26560  isdmn3  26684  dmncan1  26686  pellexlem1  26892  pellexlem6  26897  imasgim  27241  0mnnnnn0  28095  lesubnn0  28096  elfzmlbp  28107  ssfzo12  28130  elfzonelfzo  28132  2ffzoeq  28140  ccatsymb  28179  swrdtrcfv0  28195  swrdswrdlem  28198  swrdccatin1  28205  swrdccatin12lem4  28213  swrdtrcfvl  28265  usgra2pthspth  28305  ax7w15lemxAUX7  29666  l1cvpat  29852  atnle  30115  cvlexch3  30130  cvlexch4N  30131  cvlatexchb1  30132  cvrat2  30226  atlelt  30235  3dimlem4a  30260  3dimlem4OLDN  30262  ps-1  30274  ps-2  30275  4atlem10  30403  4atlem11  30406  4atlem12  30409  cdleme11c  31058  cdleme21c  31124  cdlemg6d  31418  trlcoat  31520  tendoid0  31622  cdleml3N  31775  dia2dimlem7  31868
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