Theorem simpll2 1061

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

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

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 1004

This theorem is referenced by:  fidceq  7051  fidifsnen  7052  en2eqpr  7092  iunfidisj  7136  ctssdc  7303  cauappcvgprlemlol  7857  caucvgprlemlol  7880  caucvgprprlemlol  7908  elfzonelfzo  10465  qbtwnre  10506  nn0ltexp2  10961  hashun  11058  swrdclg  11221  xrmaxltsup  11809  subcn2  11862  prodmodclem2  12128  divalglemex  12473  divalglemeuneg  12474  dvdslegcd  12525  lcmledvds  12632  modprmn0modprm0  12819  qexpz  12915  rnglidlmcl  14484  iscnp4  14932  cnrest2  14950  blssps  15141  blss  15142  bdbl  15217  metcnp3  15225  addcncntoplem  15275  cdivcncfap  15318  lgsfcl2  15725  lgsdir  15754  lgsne0  15757  clwwlknonex2  16234