Theorem 3adant1 973

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant1

Step	Hyp	Ref	Expression
1		3simpc 954	. 2 |- ((th /\ ph /\ ps) -> (ph /\ ps))
2		3adant.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	syl 15	1 |- ((th /\ ph /\ 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:  3ad2ant2  977  3ad2ant3  978  rsp2e  2678  sbciegft  3077  otkelins2kg  4254  otkelins3kg  4255  nnsucelr  4429  nndisjeq  4430  leltfintr  4459  ltfintr  4460  ncfinlower  4484  tfin11  4494  sfindbl  4531  vfinncvntnn  4549  fununiq  5518  mpt2eq3ia  5671  clos1basesuc  5883  enadj  6061  lectr  6212  leltctr  6213  lecponc  6214  taddc  6230  letc  6232  ce2le  6234  addcdi  6251  addcdir  6252  ncslemuc  6256  nchoicelem17  6306