Theorem 3simp1i 803

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

Syntax hints:   /\ w3a 787

This theorem is referenced by:  find 3212  sqrlem20 6782  bcpasc2 7058  expcnvlem2 7318  expcnvlem4 7320  ivthlem6 7376  ivthlem7 7377  ivthlem8 7378  ef01tllem2 7474  ef01tllem2OLD 7475  eflegeo 7507  efm1legeo 7509  siilem2 8596  pilem2 8755  pilem3 8756  pire 8760  pipos 8761  cosh111 8800  efghgrpilem 8802  efifolem1 8805  efifolem2 8806  efif1lem5 8817  h2hva 8926  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