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  6869  fidifsnen  6870  en2eqpr  6907  iunfidisj  6945  ctssdc  7112  cauappcvgprlemlol  7646  caucvgprlemlol  7669  caucvgprprlemlol  7697  elfzonelfzo  10230  qbtwnre  10257  nn0ltexp2  10689  hashun  10785  xrmaxltsup  11266  subcn2  11319  prodmodclem2  11585  divalglemex  11927  divalglemeuneg  11928  dvdslegcd  11965  lcmledvds  12070  modprmn0modprm0  12256  qexpz  12350  iscnp4  13721  cnrest2  13739  blssps  13930  blss  13931  bdbl  14006  metcnp3  14014  addcncntoplem  14054  cdivcncfap  14090  lgsfcl2  14410  lgsdir  14439  lgsne0  14442