Theorem 3adant3 975

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 952	. 2 |- ((ph /\ ps /\ th) -> (ph /\ ps))
2		3adant.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	syl 15	1 |- ((ph /\ ps /\ th) -> 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:  vtoclgft  2906  eqeu  3008  sikss1c1c  4268  ins2kss  4280  ins3kss  4281  leltfintr  4459  ltfintr  4460  lefinlteq  4464  ltfintri  4467  ncfineleq  4478  tfindi  4497  tfinltfin  4502  sfintfin  4533  tfinnn  4535  spfinsfincl  4540  addccan2  4560  brsi  4762  fnco  5192  resdif  5307  fnimapr  5375  f1ocnvfvb  5480  f1oiso2  5501  fununiq  5518  ovig  5598  ov2ag  5599  ov6g  5601  ovg  5602  ovmpt2x  5713  elmapg  6013  elpmg  6014  ceclr  6188  addlec  6209  lectr  6212  leaddc1  6215  nclenn  6250  addcdir  6252  lemuc1  6254  ncslemuc  6256  lecadd2  6267  spaccl  6287