Theorem 3adant2 974

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

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

Assertion

Ref	Expression
3adant2	|- ((ph /\ th /\ ps) -> ch)

Proof of Theorem 3adant2

Step	Hyp	Ref	Expression
1		3simpb 953	. 2 |- ((ph /\ th /\ ps) -> (ph /\ ps))
2		3adant.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	syl 15	1 |- ((ph /\ th /\ ps) -> ch)

Syntax hints:   -> wi 4   /\ wa 358   /\ w3a 934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936

This theorem is referenced by:  3ad2ant1  976  eupickb  2269  vtoclegft  2926  eqeu  3007  leltfintr  4458  ltfintr  4459  ltfintri  4466  ncfineleq  4477  tfinltfin  4501  vfinspnn  4541  vfintle  4546  phi11lem1  4595  fnco  5191  dff1o2  5291  fnimapr  5374  f1elima  5474  f1ocnvfvb  5479  fununiq  5517  oprssov  5603  ncspw1eu  6159  leaddc1  6214  letc  6231  addcdir  6251  lemuc1  6253  lecadd2  6266  nchoicelem17  6305