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  3086  sotr2  4492  ordtr3  4586  ordintdif  4590  tfindsg  4799  tfindsg2  4800  nnsuc  4821  findsg  4831  sossfld  5276  tz6.12i  5710  suppssr  5823  soisoi  6007  ov3  6169  tfrlem9  6605  oe0lem  6716  oa00  6761  omwordi  6773  om00  6777  omass  6782  oelim2  6797  oeoa  6799  oeoe  6801  nnmwordi  6837  swoso  6895  dom2lem  7106  onsdominel  7215  f1finf1o  7294  cantnfp1lem3  7592  cantnfp1  7593  cantnflem1  7601  rankr1ai  7680  rankval3b  7708  harcard  7821  infxpenlem  7851  alephnbtwn  7908  alephinit  7932  infxp  8051  cofsmo  8105  infpssALT  8149  fin23lem24  8158  fin56  8229  ttukeylem6  8350  ficard  8396  alephval2  8403  fpwwe2lem8  8468  fpwwe2  8474  gchcda1  8487  pwfseqlem3  8491  pwfseqlem4a  8492  pwfseqlem4  8493  gchpwdom  8505  tskss  8589  inar1  8606  gruss  8627  gruurn  8629  ltsonq  8802  distrlem4pr  8859  sqgt0sr  8937  map2psrpr  8941  letric  9130  renegcli  9318  nnge1  9982  zneo  10308  uzind2  10318  fzind  10324  nn0ind-raph  10326  uzwo  10495  uzwoOLD  10496  zbtwnre  10528  rpnnen1lem5  10560  xrletri  10700  qsqueeze  10743  difreicc  10984  om2uzf1oi  11248  facdiv  11533  facwordi  11535  bcpasc  11567  hashdom  11608  hashle00  11624  limsupbnd1  12231  lo1bdd2  12273  addcn2  12342  mulcn2  12344  o1rlimmul  12367  lo1add  12375  lo1mul  12376  rlimno1  12402  znnenlem  12766  ruclem3  12787  odd2np1  12863  bitsfzo  12902  pcdvdsb  13197  pcaddlem  13212  infpnlem1  13233  prmunb  13237  vdwlem9  13312  vdwnnlem3  13320  ramcl  13352  setcmon  14197  setcepi  14198  setciso  14201  ghmf1  14989  sylow2alem2  15207  sylow2blem3  15211  divsabl  15435  lt6abl  15459  cyggexb  15463  gsumcom2  15504  imasrng  15680  drnginvrcl  15807  drnginvrl  15809  drnginvrr  15810  subrgdvds  15837  lsmelval2  16112  divscrng  16266  mplsubrglem  16457  xrsdsreclblem  16699  obs2ss  16911  obslbs  16912  cmpsublem  17416  cmpsub  17417  1stccnp  17478  txhaus  17632  xkohaus  17638  ufilss  17890  cfinufil  17913  fmfnfmlem1  17939  hausflim  17966  fclscf  18010  alexsubb  18030  divstgplem  18103  prdsbl  18474  metss2lem  18494  nghmcn  18732  cfil3i  19175  cmetcaulem  19194  minveclem4  19286  ovolgelb  19329  ovolunnul  19349  ovoliun  19354  ovoliunnul  19356  ovolicc2lem2  19367  iundisj2  19396  voliunlem3  19399  rolle  19827  dvlip  19830  lhop1lem  19850  lhop2  19852  dvfsumrlim  19868  deg1ge  19974  coeeulem  20096  dgrco  20146  radcnvlt1  20287  psercnlem1  20294  logcnlem2  20487  logcnlem3  20488  cxpeq  20594  angpined  20624  efrlim  20761  basellem2  20817  ppieq0  20912  mumullem2  20916  chpeq0  20945  chteq0  20946  chtub  20949  fsumvma  20950  dchrptlem1  21001  bposlem6  21026  lgseisenlem2  21087  2sqlem6  21106  dchrisum0lem1  21163  pntrsumbnd2  21214  pntlem3  21256  dvrunz  21974  blocni  22259  ubthlem1  22325  minvecolem4  22335  shmodsi  22844  atcvati  23842  atcvat2i  23843  chirredlem4  23849  atmd2  23856  sumdmdlem  23874  addltmulALT  23902  iundisj2f  23983  iundisj2fi  24106  kerf1hrm  24215  dmgmaddn0  24760  lgamucov  24775  erdszelem9  24838  mulge0b  25144  rdgprc  25365  soseq  25468  colinearalg  25753  cgrsub  25883  btwnxfr  25894  lineext  25914  linecgr  25919  btwnconn1lem4  25928  btwnconn1lem5  25929  btwnconn1lem6  25930  btwnconn1lem8  25932  btwnconn1lem11  25935  ltflcei  26140  lxflflp1  26142  locfincf  26276  heiborlem6  26415  grpokerinj  26450  isdmn3  26574  dmncan1  26576  pellexlem1  26782  pellexlem6  26787  imasgim  27132  0mnnnnn0  27971  lesubnn0  27972  elfzmlbp  27978  ssfzo12  27990  elfzonelfzo  27992  swrdswrdlem  28010  swrdccatin1  28016  swrdccatin12lem3  28024  swrdccatin12c  28028  swrdccat3  28029  usgra2pthspth  28035  l1cvpat  29537  atnle  29800  cvlexch3  29815  cvlexch4N  29816  cvlatexchb1  29817  cvrat2  29911  atlelt  29920  3dimlem4a  29945  3dimlem4OLDN  29947  ps-1  29959  ps-2  29960  4atlem10  30088  4atlem11  30091  4atlem12  30094  cdleme11c  30743  cdleme21c  30809  cdlemg6d  31103  trlcoat  31205  tendoid0  31307  cdleml3N  31460  dia2dimlem7  31553
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