Theorem simpll2 1021

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  fidceq  6763  fidifsnen  6764  en2eqpr  6801  iunfidisj  6834  ctssdc  6998  cauappcvgprlemlol  7455  caucvgprlemlol  7478  caucvgprprlemlol  7506  elfzonelfzo  10007  qbtwnre  10034  hashun  10551  xrmaxltsup  11027  subcn2  11080  prodmodclem2  11346  divalglemex  11619  divalglemeuneg  11620  dvdslegcd  11653  lcmledvds  11751  iscnp4  12387  cnrest2  12405  blssps  12596  blss  12597  bdbl  12672  metcnp3  12680  addcncntoplem  12720  cdivcncfap  12756