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

Theorem sylbird 228
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 216 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbird.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 43 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3imtr3d  260  eqreu  3135  sotr2  4567  ordtr3  4661  ordintdif  4665  tfindsg  4875  tfindsg2  4876  nnsuc  4897  findsg  4907  sossfld  5352  tz6.12i  5782  suppssr  5900  soisoi  6084  ov3  6246  tfrlem9  6682  oe0lem  6793  oa00  6838  omwordi  6850  om00  6854  omass  6859  oelim2  6874  oeoa  6876  oeoe  6878  nnmwordi  6914  swoso  6972  dom2lem  7183  onsdominel  7292  f1finf1o  7371  cantnfp1lem3  7672  cantnfp1  7673  cantnflem1  7681  rankr1ai  7760  rankval3b  7788  harcard  7903  infxpenlem  7933  alephnbtwn  7990  alephinit  8014  infxp  8133  cofsmo  8187  infpssALT  8231  fin23lem24  8240  fin56  8311  ttukeylem6  8432  ficard  8478  alephval2  8485  fpwwe2lem8  8550  fpwwe2  8556  gchcda1  8569  pwfseqlem3  8573  pwfseqlem4a  8574  pwfseqlem4  8575  gchpwdom  8583  tskss  8671  inar1  8688  gruss  8709  gruurn  8711  ltsonq  8884  distrlem4pr  8941  sqgt0sr  9019  map2psrpr  9023  letric  9212  renegcli  9400  nnge1  10064  zneo  10390  uzind2  10400  fzind  10406  nn0ind-raph  10408  uzwo  10577  uzwoOLD  10578  zbtwnre  10610  rpnnen1lem5  10642  xrletri  10782  qsqueeze  10825  difreicc  11066  om2uzf1oi  11331  facdiv  11616  facwordi  11618  bcpasc  11650  hashdom  11691  hashle00  11707  limsupbnd1  12314  lo1bdd2  12356  addcn2  12425  mulcn2  12427  o1rlimmul  12450  lo1add  12458  lo1mul  12459  rlimno1  12485  znnenlem  12849  ruclem3  12870  odd2np1  12946  bitsfzo  12985  pcdvdsb  13280  pcaddlem  13295  infpnlem1  13316  prmunb  13320  vdwlem9  13395  vdwnnlem3  13403  ramcl  13435  setcmon  14280  setcepi  14281  setciso  14284  ghmf1  15072  sylow2alem2  15290  sylow2blem3  15294  divsabl  15518  lt6abl  15542  cyggexb  15546  gsumcom2  15587  imasrng  15763  drnginvrcl  15890  drnginvrl  15892  drnginvrr  15893  subrgdvds  15920  lsmelval2  16195  divscrng  16349  mplsubrglem  16540  xrsdsreclblem  16782  obs2ss  16994  obslbs  16995  cmpsublem  17500  cmpsub  17501  1stccnp  17563  txhaus  17717  xkohaus  17723  ufilss  17975  cfinufil  17998  fmfnfmlem1  18024  hausflim  18051  fclscf  18095  alexsubb  18115  divstgplem  18188  prdsbl  18559  metss2lem  18579  nghmcn  18817  cfil3i  19260  cmetcaulem  19279  minveclem4  19371  ovolgelb  19414  ovolunnul  19434  ovoliun  19439  ovoliunnul  19441  ovolicc2lem2  19452  iundisj2  19481  voliunlem3  19484  rolle  19912  dvlip  19915  lhop1lem  19935  lhop2  19937  dvfsumrlim  19953  deg1ge  20059  coeeulem  20181  dgrco  20231  radcnvlt1  20372  psercnlem1  20379  logcnlem2  20572  logcnlem3  20573  cxpeq  20679  angpined  20709  efrlim  20846  basellem2  20902  ppieq0  20997  mumullem2  21001  chpeq0  21030  chteq0  21031  chtub  21034  fsumvma  21035  dchrptlem1  21086  bposlem6  21111  lgseisenlem2  21172  2sqlem6  21191  dchrisum0lem1  21248  pntrsumbnd2  21299  pntlem3  21341  dvrunz  22059  blocni  22344  ubthlem1  22410  minvecolem4  22420  shmodsi  22929  atcvati  23927  atcvat2i  23928  chirredlem4  23934  atmd2  23941  sumdmdlem  23959  addltmulALT  23987  iundisj2f  24065  iundisj2fi  24188  kerf1hrm  24297  dmgmaddn0  24842  lgamucov  24857  erdszelem9  24920  mulge0b  25226  rdgprc  25457  soseq  25564  colinearalg  25884  cgrsub  26014  btwnxfr  26025  lineext  26045  linecgr  26050  btwnconn1lem4  26059  btwnconn1lem5  26060  btwnconn1lem6  26061  btwnconn1lem8  26063  btwnconn1lem11  26066  ltflcei  26275  lxflflp1  26277  ftc1anclem5  26326  locfincf  26428  heiborlem6  26567  grpokerinj  26602  isdmn3  26726  dmncan1  26728  pellexlem1  27004  pellexlem6  27009  imasgim  27353  0mnnnnn0  28216  lesubnn0  28217  elfzmlbp  28228  ssfzo12  28251  elfzonelfzo  28253  2ffzoeq  28261  ccatsymb  28309  swrdtrcfv0  28327  swrdswrdlem  28330  swrdccatin1  28337  swrdccatin12lem4  28345  swrdtrcfvl  28397  usgra2pthspth  28441  nbhashuvtx1  28529  ax7w15lemxAUX7  29840  l1cvpat  30026  atnle  30289  cvlexch3  30304  cvlexch4N  30305  cvlatexchb1  30306  cvrat2  30400  atlelt  30409  3dimlem4a  30434  3dimlem4OLDN  30436  ps-1  30448  ps-2  30449  4atlem10  30577  4atlem11  30580  4atlem12  30583  cdleme11c  31232  cdleme21c  31298  cdlemg6d  31592  trlcoat  31694  tendoid0  31796  cdleml3N  31949  dia2dimlem7  32042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator