Theorem simpll2 1027

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

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

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 970

This theorem is referenced by:  fidceq  6831  fidifsnen  6832  en2eqpr  6869  iunfidisj  6907  ctssdc  7074  cauappcvgprlemlol  7584  caucvgprlemlol  7607  caucvgprprlemlol  7635  elfzonelfzo  10161  qbtwnre  10188  nn0ltexp2  10619  hashun  10714  xrmaxltsup  11195  subcn2  11248  prodmodclem2  11514  divalglemex  11855  divalglemeuneg  11856  dvdslegcd  11893  lcmledvds  11998  modprmn0modprm0  12184  qexpz  12278  iscnp4  12818  cnrest2  12836  blssps  13027  blss  13028  bdbl  13103  metcnp3  13111  addcncntoplem  13151  cdivcncfap  13187  lgsfcl2  13507  lgsdir  13536  lgsne0  13539