Theorem simpll2 1040

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 1004	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

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 983

This theorem is referenced by:  fidceq  6987  fidifsnen  6988  en2eqpr  7025  iunfidisj  7069  ctssdc  7236  cauappcvgprlemlol  7790  caucvgprlemlol  7813  caucvgprprlemlol  7841  elfzonelfzo  10391  qbtwnre  10431  nn0ltexp2  10886  hashun  10982  swrdclg  11136  xrmaxltsup  11654  subcn2  11707  prodmodclem2  11973  divalglemex  12318  divalglemeuneg  12319  dvdslegcd  12370  lcmledvds  12477  modprmn0modprm0  12664  qexpz  12760  rnglidlmcl  14327  iscnp4  14775  cnrest2  14793  blssps  14984  blss  14985  bdbl  15060  metcnp3  15068  addcncntoplem  15118  cdivcncfap  15161  lgsfcl2  15568  lgsdir  15597  lgsne0  15600