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

Step	Hyp	Ref	Expression
1		simpl2 1001	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

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