Theorem 3simp3i 883

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

Syntax hints:   /\ w3a 855

This theorem is referenced by:  sqrlem20 7737  bcpasc2 8015  expcnvlem2 8284  expcnvlem4 8286  ivthlem7 8344  ivthlem8 8345  ef01tllem2 8441  ef01tllem2OLD 8442  eflegeo 8476  efm1legeo 8478  siilem2 9648  pilem2 9816  pilem3 9817  sinpi 9820  cosh111 9866  efifolem1 9871  dfrelog 9905  h2hnm 10269  elunop2 11367  divalglem6 13493  fsumleisumi 15508  trirn 15516  piececn 15576

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 163  df-an 241  df-3an 857

Copyright terms: Public domain