Theorem 3simp1i 881

Description: Infer a conjunct from a triple conjunction.

Hypothesis

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

Assertion

Ref	Expression
3simp1i	|- ph

Proof of Theorem 3simp1i

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

Syntax hints:   /\ w3a 855

This theorem is referenced by:  find 3788  findOLD 3789  sqrlem20 7737  bcpasc2 8015  expcnvlem2 8284  expcnvlem4 8286  ivthlem6 8343  ivthlem7 8344  ivthlem8 8345  ef01tllem2 8441  ef01tllem2OLD 8442  eflegeo 8476  efm1legeo 8478  siilem2 9648  pilem2 9816  pilem3 9817  pire 9821  pipos 9822  cosh111 9866  efghgrpilem 9868  efifolem1 9871  efifolem2 9872  efif1lem5 9883  h2hva 10267  elunop2 11367  divalglem6 13493  fsumleisumi 15508  trirn 15516

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