Theorem simpll2 1039

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

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

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 982

This theorem is referenced by:  fidceq  6927  fidifsnen  6928  en2eqpr  6965  iunfidisj  7007  ctssdc  7174  cauappcvgprlemlol  7709  caucvgprlemlol  7732  caucvgprprlemlol  7760  elfzonelfzo  10300  qbtwnre  10328  nn0ltexp2  10783  hashun  10879  xrmaxltsup  11404  subcn2  11457  prodmodclem2  11723  divalglemex  12066  divalglemeuneg  12067  dvdslegcd  12104  lcmledvds  12211  modprmn0modprm0  12397  qexpz  12493  rnglidlmcl  13979  iscnp4  14397  cnrest2  14415  blssps  14606  blss  14607  bdbl  14682  metcnp3  14690  addcncntoplem  14740  cdivcncfap  14783  lgsfcl2  15163  lgsdir  15192  lgsne0  15195