Theorem simpll2 1063

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

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

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 1006

This theorem is referenced by:  fidceq  7056  fidifsnen  7057  en2eqpr  7099  iunfidisj  7145  ctssdc  7312  cauappcvgprlemlol  7867  caucvgprlemlol  7890  caucvgprprlemlol  7918  elfzonelfzo  10476  qbtwnre  10517  nn0ltexp2  10972  hashun  11069  swrdclg  11235  xrmaxltsup  11836  subcn2  11889  prodmodclem2  12156  divalglemex  12501  divalglemeuneg  12502  dvdslegcd  12553  lcmledvds  12660  modprmn0modprm0  12847  qexpz  12943  rnglidlmcl  14513  iscnp4  14961  cnrest2  14979  blssps  15170  blss  15171  bdbl  15246  metcnp3  15254  addcncntoplem  15304  cdivcncfap  15347  lgsfcl2  15754  lgsdir  15783  lgsne0  15786  subupgr  16143  clwwlknonex2  16309