Theorem 3simp3i 791

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

Syntax hints:   /\ w3a 773

This theorem is referenced by:  sqrlem20 6622  bcpasc2t 6906  expcnvlem2 7163  expcnvlem4 7165  ivthlem7 7222  ivthlem8 7223  ivthlem7OLD 7231  ivthlem8OLD 7232  ef01tllem2 7326  eflegeot 7356  efm1legeot 7358  siilem2 8443  pilem2 8591  pilem3 8592  sinpi 8595  cosh111t 8632  efifolem1 8637  dfrelog 8678  h2hnm 8784  elunop2t 9853

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