Theorem 3simp3i 792

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

Syntax hints:   /\ w3a 774

This theorem is referenced by:  sqrlem20 6637  bcpasc2t 6921  expcnvlem2 7180  expcnvlem4 7182  ivthlem7 7239  ivthlem8 7240  ivthlem7OLD 7248  ivthlem8OLD 7249  ef01tllem2 7343  eflegeot 7373  efm1legeot 7375  siilem2 8471  pilem2 8626  pilem3 8627  sinpi 8630  cosh111t 8667  efifolem1 8672  dfrelog 8711  h2hnm 8800  elunop2t 9894

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 776

Copyright terms: Public domain