Theorem 3simp3i 805

Description: Infer a conjunct from a triple conjunction.

Hypothesis

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

Assertion

Ref	Expression
3simp3i	|- ch

Proof of Theorem 3simp3i

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

Syntax hints:   /\ w3a 787

This theorem is referenced by:  sqrlem20 6782  bcpasc2 7058  expcnvlem2 7318  expcnvlem4 7320  ivthlem7 7377  ivthlem8 7378  ef01tllem2 7474  ef01tllem2OLD 7475  eflegeo 7507  efm1legeo 7509  siilem2 8596  pilem2 8755  pilem3 8756  sinpi 8759  cosh111 8800  efifolem1 8805  dfrelog 8839  h2hnm 8928  elunop2 10021

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