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

Theorem sylbird 235
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 223 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbird.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 44 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3imtr3d  267  ceqex  3195  eqreu  3256  sotr2  4777  ordtr3  4871  ordintdif  4875  sossfld  5392  tz6.12i  5818  suppssrOLD  5945  soisoi  6127  ov3  6336  tfindsg  6580  tfindsg2  6581  nnsuc  6602  findsg  6612  suppssr  6829  tfrlem9  6953  oe0lem  7062  oa00  7107  omwordi  7119  om00  7123  omass  7128  oelim2  7143  oeoa  7145  oeoe  7147  nnmwordi  7183  swoso  7241  dom2lem  7458  onsdominel  7569  f1finf1o  7649  cantnfp1lem3  7998  cantnfp1  7999  cantnflem1  8007  cantnfp1lem3OLD  8024  cantnfp1OLD  8025  cantnflem1OLD  8030  rankr1ai  8115  rankval3b  8143  harcard  8258  infxpenlem  8290  alephnbtwn  8351  alephinit  8375  infxp  8494  cofsmo  8548  infpssALT  8592  fin23lem24  8601  fin56  8672  ttukeylem6  8793  ficard  8839  alephval2  8846  fpwwe2lem8  8914  fpwwe2  8920  gchcda1  8933  pwfseqlem3  8937  pwfseqlem4a  8938  pwfseqlem4  8939  gchpwdom  8947  tskss  9035  inar1  9052  gruss  9073  gruurn  9075  ltsonq  9248  distrlem4pr  9305  sqgt0sr  9383  map2psrpr  9387  letric  9585  renegcli  9780  mulge0b  10309  nnge1  10458  0mnnnnn0  10722  zneo  10834  uzind2  10844  fzind  10850  nn0ind-raph  10852  uzwo  11027  uzwoOLD  11028  zbtwnre  11061  rpnnen1lem5  11093  xrletri  11238  qsqueeze  11281  difreicc  11533  elfzmlbp  11607  elfzodifsumelfzo  11720  ssfzo12  11736  elfzonelfzo  11743  fleqceilz  11809  om2uzf1oi  11892  facdiv  12179  facwordi  12181  bcpasc  12213  hashdom  12259  hashle00  12275  lswcl  12387  ccatsymb  12398  ccatval1lsw  12400  swrdspsleq  12459  swrdlsw  12463  swrdswrdlem  12470  swrdccatin1  12491  swrdccatin12lem3  12498  repswswrd  12539  cshwidx0  12559  limsupbnd1  13077  lo1bdd2  13119  addcn2  13188  mulcn2  13190  o1rlimmul  13213  lo1add  13221  lo1mul  13222  rlimno1  13248  znnenlem  13611  ruclem3  13632  odd2np1  13709  bitsfzo  13748  pcdvdsb  14052  pcaddlem  14067  infpnlem1  14088  prmunb  14092  vdwlem9  14167  vdwnnlem3  14175  ramcl  14207  cshwshash  14248  setcmon  15073  setcepi  15074  setciso  15077  ghmf1  15893  sylow2alem2  16237  sylow2blem3  16241  divsabl  16467  lt6abl  16491  cyggexb  16495  gsumcom2  16588  imasrng  16833  f1rhm0to0  16950  drnginvrcl  16971  drnginvrl  16973  drnginvrr  16974  subrgdvds  17001  lsmelval2  17288  divscrng  17444  mplsubrglem  17640  mplsubrglemOLD  17641  xrsdsreclblem  17983  obs2ss  18278  obslbs  18279  cmpsublem  19133  cmpsub  19134  1stccnp  19197  txhaus  19351  xkohaus  19357  ufilss  19609  cfinufil  19632  fmfnfmlem1  19658  hausflim  19685  fclscf  19729  alexsubb  19749  divstgplem  19822  prdsbl  20197  metss2lem  20217  nghmcn  20455  cfil3i  20911  cmetcaulem  20930  minveclem4  21050  ovolgelb  21094  ovolunnul  21114  ovoliun  21119  ovoliunnul  21121  ovolicc2lem2  21132  iundisj2  21162  voliunlem3  21165  rolle  21594  dvlip  21597  lhop1lem  21617  lhop2  21619  dvfsumrlim  21635  deg1ge  21702  coeeulem  21824  dgrco  21874  radcnvlt1  22015  psercnlem1  22022  logcnlem2  22220  logcnlem3  22221  cxpeq  22327  angpined  22357  efrlim  22495  basellem2  22551  ppieq0  22646  mumullem2  22650  chpeq0  22679  chteq0  22680  chtub  22683  fsumvma  22684  dchrptlem1  22735  bposlem6  22760  lgseisenlem2  22821  2sqlem6  22840  dchrisum0lem1  22897  pntrsumbnd2  22948  pntlem3  22990  colinearalg  23307  eengtrkg  23382  dvrunz  24071  blocni  24356  ubthlem1  24422  minvecolem4  24432  shmodsi  24943  atcvati  25941  atcvat2i  25942  chirredlem4  25948  atmd2  25955  sumdmdlem  25973  addltmulALT  26001  iundisj2f  26082  iundisj2fi  26225  dmgmaddn0  27152  lgamucov  27167  erdszelem9  27230  rdgprc  27751  soseq  27858  cgrsub  28219  btwnxfr  28230  lineext  28250  linecgr  28255  btwnconn1lem4  28264  btwnconn1lem5  28265  btwnconn1lem6  28266  btwnconn1lem8  28268  btwnconn1lem11  28271  ltflcei  28566  lxflflp1  28568  ftc1anclem5  28618  locfincf  28725  heiborlem6  28862  grpokerinj  28897  isdmn3  29021  dmncan1  29023  pellexlem1  29317  pellexlem6  29322  imasgim  29602  lesubnn0  30328  nn0lt2  30333  nn01to3  30334  2ffzoeq  30361  elfzom1elp1fzo  30365  prmn2uzge3  30396  wlkv0  30438  usgra2pthspth  30442  0clwlk  30575  clwwlkgt0  30581  clwlkisclwwlklem2a4  30593  clwlkisclwwlklem1  30596  zm1nn  30615  erclwwlktr0  30626  difelfznle  30635  nbhashuvtx1  30680  ztprmneprm  30886  lmod0rng  30926  gsummoncoe1  30995  lincresunit3  31133  mp2pm2mplem4  31281  chfacfisf  31325  chfacfisfcpmat  31326  cayleyhamilton1  31364  l1cvpat  33022  atnle  33285  cvlexch3  33300  cvlexch4N  33301  cvlatexchb1  33302  cvrat2  33396  atlelt  33405  3dimlem4a  33430  3dimlem4OLDN  33432  ps-1  33444  ps-2  33445  4atlem10  33573  4atlem11  33576  4atlem12  33579  cdleme11c  34228  cdleme21c  34294  cdlemg6d  34588  trlcoat  34690  tendoid0  34792  cdleml3N  34945  dia2dimlem7  35038
  Copyright terms: Public domain W3C validator