Theorem simpl3r 932

Description: Simplification of conjunction.

Assertion

Ref	Expression
simpl3r	|- (((ch /\ th /\ (ph /\ ps)) /\ ta) -> ps)

Proof of Theorem simpl3r

Step	Hyp	Ref	Expression
1		simp3r 905	. 2 |- ((ch /\ th /\ (ph /\ ps)) -> ps)
2	1	adantr 425	1 |- (((ch /\ th /\ (ph /\ ps)) /\ ta) -> ps)

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  ssblex 9133  idmon 15166  iccss 15855  cvrcmp 16999  atcvrj2b 17069  ps2 17079  paddasslem8 17288  paddasslem9 17289  paddasslem10 17290  paddasslem12 17292  paddasslem13 17293

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain