Theorem 3simp2i 882

Description: Infer a conjunct from a triple conjunction.

Hypothesis

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

Assertion

Ref	Expression
3simp2i	|- ps

Proof of Theorem 3simp2i

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

Syntax hints:   /\ w3a 855

This theorem is referenced by:  sqrlem20 7737  bcpasc2 8015  expcnvlem2 8284  expcnvlem4 8286  ivthlem6 8343  ivthlem7 8344  ivthlem8 8345  ef01tllem2 8441  ef01tllem2OLD 8442  eflegeo 8476  efm1legeo 8478  ghsubgi 9241  siilem2 9648  pilem2 9816  pigt2lt4 9819  cosh111 9866  efghgrpilem 9868  efifolem1 9871  hhssabli 10557  elunop2 11367  cayleylem3 13435  divalglem6 13493  rrisgrp 14421  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