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  6925  fidifsnen  6926  en2eqpr  6963  iunfidisj  7005  ctssdc  7172  cauappcvgprlemlol  7707  caucvgprlemlol  7730  caucvgprprlemlol  7758  elfzonelfzo  10297  qbtwnre  10325  nn0ltexp2  10780  hashun  10876  xrmaxltsup  11401  subcn2  11454  prodmodclem2  11720  divalglemex  12063  divalglemeuneg  12064  dvdslegcd  12101  lcmledvds  12208  modprmn0modprm0  12394  qexpz  12490  rnglidlmcl  13976  iscnp4  14386  cnrest2  14404  blssps  14595  blss  14596  bdbl  14671  metcnp3  14679  addcncntoplem  14719  cdivcncfap  14758  lgsfcl2  15122  lgsdir  15151  lgsne0  15154