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  3079  eqreu  3140  sotr2  4657  ordtr3  4751  ordintdif  4755  sossfld  5273  tz6.12i  5698  suppssrOLD  5825  soisoi  6006  ov3  6216  tfindsg  6460  tfindsg2  6461  nnsuc  6482  findsg  6492  suppssr  6709  tfrlem9  6830  oe0lem  6941  oa00  6986  omwordi  6998  om00  7002  omass  7007  oelim2  7022  oeoa  7024  oeoe  7026  nnmwordi  7062  swoso  7120  dom2lem  7337  onsdominel  7448  f1finf1o  7527  cantnfp1lem3  7876  cantnfp1  7877  cantnflem1  7885  cantnfp1lem3OLD  7902  cantnfp1OLD  7903  cantnflem1OLD  7908  rankr1ai  7993  rankval3b  8021  harcard  8136  infxpenlem  8168  alephnbtwn  8229  alephinit  8253  infxp  8372  cofsmo  8426  infpssALT  8470  fin23lem24  8479  fin56  8550  ttukeylem6  8671  ficard  8717  alephval2  8724  fpwwe2lem8  8792  fpwwe2  8798  gchcda1  8811  pwfseqlem3  8815  pwfseqlem4a  8816  pwfseqlem4  8817  gchpwdom  8825  tskss  8913  inar1  8930  gruss  8951  gruurn  8953  ltsonq  9126  distrlem4pr  9183  sqgt0sr  9261  map2psrpr  9265  letric  9463  renegcli  9658  mulge0b  10187  nnge1  10336  0mnnnnn0  10600  zneo  10712  uzind2  10722  fzind  10728  nn0ind-raph  10730  uzwo  10905  uzwoOLD  10906  zbtwnre  10939  rpnnen1lem5  10971  xrletri  11116  qsqueeze  11159  difreicc  11404  elfzmlbp  11478  elfzodifsumelfzo  11588  ssfzo12  11604  elfzonelfzo  11611  fleqceilz  11677  om2uzf1oi  11760  facdiv  12047  facwordi  12049  bcpasc  12081  hashdom  12126  hashle00  12142  lswcl  12254  ccatsymb  12265  ccatval1lsw  12267  swrdspsleq  12326  swrdlsw  12330  swrdswrdlem  12337  swrdccatin1  12358  swrdccatin12lem3  12365  repswswrd  12406  cshwidx0  12426  limsupbnd1  12944  lo1bdd2  12986  addcn2  13055  mulcn2  13057  o1rlimmul  13080  lo1add  13088  lo1mul  13089  rlimno1  13115  znnenlem  13477  ruclem3  13498  odd2np1  13575  bitsfzo  13614  pcdvdsb  13918  pcaddlem  13933  infpnlem1  13954  prmunb  13958  vdwlem9  14033  vdwnnlem3  14041  ramcl  14073  cshwshash  14114  setcmon  14938  setcepi  14939  setciso  14942  ghmf1  15755  sylow2alem2  16097  sylow2blem3  16101  divsabl  16327  lt6abl  16351  cyggexb  16355  gsumcom2  16441  imasrng  16646  drnginvrcl  16773  drnginvrl  16775  drnginvrr  16776  subrgdvds  16803  lsmelval2  17088  divscrng  17244  mplsubrglem  17451  mplsubrglemOLD  17452  xrsdsreclblem  17703  obs2ss  17996  obslbs  17997  cmpsublem  18844  cmpsub  18845  1stccnp  18908  txhaus  19062  xkohaus  19068  ufilss  19320  cfinufil  19343  fmfnfmlem1  19369  hausflim  19396  fclscf  19440  alexsubb  19460  divstgplem  19533  prdsbl  19908  metss2lem  19928  nghmcn  20166  cfil3i  20622  cmetcaulem  20641  minveclem4  20761  ovolgelb  20805  ovolunnul  20825  ovoliun  20830  ovoliunnul  20832  ovolicc2lem2  20843  iundisj2  20872  voliunlem3  20875  rolle  21304  dvlip  21307  lhop1lem  21327  lhop2  21329  dvfsumrlim  21345  deg1ge  21455  coeeulem  21577  dgrco  21627  radcnvlt1  21768  psercnlem1  21775  logcnlem2  21973  logcnlem3  21974  cxpeq  22080  angpined  22110  efrlim  22248  basellem2  22304  ppieq0  22399  mumullem2  22403  chpeq0  22432  chteq0  22433  chtub  22436  fsumvma  22437  dchrptlem1  22488  bposlem6  22513  lgseisenlem2  22574  2sqlem6  22593  dchrisum0lem1  22650  pntrsumbnd2  22701  pntlem3  22743  colinearalg  22979  eengtrkg  23054  dvrunz  23743  blocni  24028  ubthlem1  24094  minvecolem4  24104  shmodsi  24615  atcvati  25613  atcvat2i  25614  chirredlem4  25620  atmd2  25627  sumdmdlem  25645  addltmulALT  25673  iundisj2f  25756  iundisj2fi  25904  kerf1hrm  26145  dmgmaddn0  26857  lgamucov  26872  erdszelem9  26935  rdgprc  27455  soseq  27562  cgrsub  27923  btwnxfr  27934  lineext  27954  linecgr  27959  btwnconn1lem4  27968  btwnconn1lem5  27969  btwnconn1lem6  27970  btwnconn1lem8  27972  btwnconn1lem11  27975  ltflcei  28263  lxflflp1  28265  ftc1anclem5  28315  locfincf  28422  heiborlem6  28559  grpokerinj  28594  isdmn3  28718  dmncan1  28720  pellexlem1  29015  pellexlem6  29020  imasgim  29300  lesubnn0  30027  nn0lt2  30032  nn01to3  30033  2ffzoeq  30060  elfzom1elp1fzo  30064  prmn2uzge3  30095  wlkv0  30137  usgra2pthspth  30141  0clwlk  30274  clwwlkgt0  30280  clwlkisclwwlklem2a4  30292  clwlkisclwwlklem1  30295  zm1nn  30314  erclwwlktr0  30325  difelfznle  30334  nbhashuvtx1  30379  ztprmneprm  30583  lmod0rng  30610  lincresunit3  30724  l1cvpat  32272  atnle  32535  cvlexch3  32550  cvlexch4N  32551  cvlatexchb1  32552  cvrat2  32646  atlelt  32655  3dimlem4a  32680  3dimlem4OLDN  32682  ps-1  32694  ps-2  32695  4atlem10  32823  4atlem11  32826  4atlem12  32829  cdleme11c  33478  cdleme21c  33544  cdlemg6d  33838  trlcoat  33940  tendoid0  34042  cdleml3N  34195  dia2dimlem7  34288
  Copyright terms: Public domain W3C validator