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  6965  fidifsnen  6966  en2eqpr  7003  iunfidisj  7047  ctssdc  7214  cauappcvgprlemlol  7759  caucvgprlemlol  7782  caucvgprprlemlol  7810  elfzonelfzo  10357  qbtwnre  10397  nn0ltexp2  10852  hashun  10948  xrmaxltsup  11540  subcn2  11593  prodmodclem2  11859  divalglemex  12204  divalglemeuneg  12205  dvdslegcd  12256  lcmledvds  12363  modprmn0modprm0  12550  qexpz  12646  rnglidlmcl  14213  iscnp4  14661  cnrest2  14679  blssps  14870  blss  14871  bdbl  14946  metcnp3  14954  addcncntoplem  15004  cdivcncfap  15047  lgsfcl2  15454  lgsdir  15483  lgsne0  15486