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  2927  eqeu  3008  leltfintr  4459  ltfintr  4460  ltfintri  4467  ncfineleq  4478  tfinltfin  4502  vfinspnn  4542  vfintle  4547  phi11lem1  4596  fnco  5192  dff1o2  5292  fnimapr  5375  f1elima  5475  f1ocnvfvb  5480  fununiq  5518  oprssov  5604  ncspw1eu  6160  leaddc1  6215  letc  6232  addcdir  6252  lemuc1  6254  lecadd2  6267  nchoicelem17  6306