Theorem 3simp2i 790

Description: Infer a conjunct from a triple conjunction.

Hypothesis

Ref	Expression
3simp1i.1	|- (ph /\ ps /\ ch)

Assertion

Ref	Expression
3simp2i	|- ps

Proof of Theorem 3simp2i

Step	Hyp	Ref	Expression
1		3simp1i.1	. 2 |- (ph /\ ps /\ ch)
2		3simp2 787	. 2 |- ((ph /\ ps /\ ch) -> ps)
3	1, 2	ax-mp 7	1 |- ps

Syntax hints:   /\ w3a 773

This theorem is referenced by:  sqrlem20 6622  bcpasc2t 6906  expcnvlem2 7163  expcnvlem4 7165  ivthlem6 7221  ivthlem7 7222  ivthlem8 7223  ivthlem6OLD 7230  ivthlem7OLD 7231  ivthlem8OLD 7232  ivth2OLD 7234  ef01tllem2 7326  eflegeot 7356  efm1legeot 7358  ghsubgi 8075  siilem2 8443  pilem2 8591  pigt2lt4 8594  cosh111t 8632  efghgrpilem 8634  efifolem1 8637  hhssabl 9053  elunop2t 9853  cayleylem3 10318

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 147  df-an 225  df-3an 775

Copyright terms: Public domain