Theorem 3simp2i 804

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 801	. 2 |- ((ph /\ ps /\ ch) -> ps)
3	1, 2	ax-mp 7	1 |- ps

Syntax hints:   /\ w3a 787

This theorem is referenced by:  sqrlem20 6782  bcpasc2 7058  expcnvlem2 7318  expcnvlem4 7320  ivthlem6 7376  ivthlem7 7377  ivthlem8 7378  ef01tllem2 7474  ef01tllem2OLD 7475  eflegeo 7507  efm1legeo 7509  ghsubgi 8222  siilem2 8596  pilem2 8755  pigt2lt4 8758  cosh111 8800  efghgrpilem 8802  efifolem1 8805  hhssabli 9215  elunop2 10021  cayleylem3 10496

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 154  df-an 232  df-3an 789

Copyright terms: Public domain