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

Theorem simp1i 1014
Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
Hypothesis
Ref Expression
3simp1i.1  |-  ( ph  /\ 
ps  /\  ch )
Assertion
Ref Expression
simp1i  |-  ph

Proof of Theorem simp1i
StepHypRef Expression
1 3simp1i.1 . 2  |-  ( ph  /\ 
ps  /\  ch )
2 simp1 1005 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
31, 2ax-mp 5 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  find  6732  hartogslem2  8058  harwdom  8105  divalglem6  14354  structfn  15097  strleun  15182  birthday  23745  divsqrsumf  23771  emcl  23793  lgslem4  24090  lgscllem  24094  lgsdir2lem2  24115  mulog2sumlem1  24235  siilem2  26338  h2hva  26462  h2hsm  26463  elunop2  27501  wallispilem3  37498  wallispilem4  37499
  Copyright terms: Public domain W3C validator