ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpll2 Unicode version

Theorem simpll2 1037
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll2  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )

Proof of Theorem simpll2
StepHypRef Expression
1 simpl2 1001 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantr 276 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  fidceq  6868  fidifsnen  6869  en2eqpr  6906  iunfidisj  6944  ctssdc  7111  cauappcvgprlemlol  7645  caucvgprlemlol  7668  caucvgprprlemlol  7696  elfzonelfzo  10229  qbtwnre  10256  nn0ltexp2  10688  hashun  10784  xrmaxltsup  11265  subcn2  11318  prodmodclem2  11584  divalglemex  11926  divalglemeuneg  11927  dvdslegcd  11964  lcmledvds  12069  modprmn0modprm0  12255  qexpz  12349  iscnp4  13654  cnrest2  13672  blssps  13863  blss  13864  bdbl  13939  metcnp3  13947  addcncntoplem  13987  cdivcncfap  14023  lgsfcl2  14343  lgsdir  14372  lgsne0  14375
  Copyright terms: Public domain W3C validator