Theorem 3simp1i 791

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

Syntax hints:   /\ w3a 775

This theorem is referenced by:  find 3155  sqrlem20 6692  bcpasc2t 6968  expcnvlem2 7228  expcnvlem4 7230  ivthlem6 7286  ivthlem7 7287  ivthlem8 7288  ef01tllem2 7384  ef01tllem2OLD 7385  eflegeot 7416  efm1legeot 7418  siilem2 8512  pilem2 8672  pilem3 8673  pire 8677  pipos 8678  cosh111t 8717  efghgrpilem 8719  efifolem1 8722  efifolem2 8723  efif1lem5 8734  h2hva 8843  elunop2t 9938

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 777

Copyright terms: Public domain