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

Theorem simpll2 1006
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 970 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantr 274 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  fidceq  6731  fidifsnen  6732  en2eqpr  6769  iunfidisj  6802  ctssdc  6966  cauappcvgprlemlol  7423  caucvgprlemlol  7446  caucvgprprlemlol  7474  elfzonelfzo  9975  qbtwnre  10002  hashun  10519  xrmaxltsup  10995  subcn2  11048  divalglemex  11546  divalglemeuneg  11547  dvdslegcd  11580  lcmledvds  11678  iscnp4  12314  cnrest2  12332  blssps  12523  blss  12524  bdbl  12599  metcnp3  12607  addcncntoplem  12647  cdivcncfap  12683
  Copyright terms: Public domain W3C validator