Theorem 3ad2ant1 976

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	|- (ph -> ch)

Assertion

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

Proof of Theorem 3ad2ant1

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- (ph -> ch)
2	1	adantr 451	. 2 |- ((ph /\ th) -> ch)
3	2	3adant2 974	1 |- ((ph /\ ps /\ th) -> ch)

Syntax hints:   -> wi 4   /\ 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:  simp1l  979  simp1r  980  simp11  985  simp12  986  simp13  987  simp1ll  1018  simp1lr  1019  simp1rl  1020  simp1rr  1021  simp1l1  1048  simp1l2  1049  simp1l3  1050  simp1r1  1051  simp1r2  1052  simp1r3  1053  simp11l  1066  simp11r  1067  simp12l  1068  simp12r  1069  simp13l  1070  simp13r  1071  simp111  1084  simp112  1085  simp113  1086  simp121  1087  simp122  1088  simp123  1089  simp131  1090  simp132  1091  simp133  1092  3anim123i  1137  3jaao  1249  ceqsalt  2882  sbciegft  3077  reupick2  3542  otkelins2kg  4254  otkelins3kg  4255  nnsucelrlem3  4427  ssfin  4471  ncfinlower  4484  tfin11  4494  nnpweq  4524  sfinltfin  4536  vfintle  4547  vfinncvntnn  4549  peano4  4558  funprg  5150  funprgOLD  5151  fvun1  5380  fvopab4t  5386  po0  5940  nenpw1pwlem2  6086  ceclnn1  6190  nclenc  6223  lenc  6224  taddc  6230  letc  6232  nclenn  6250  addcdi  6251  spaccl  6287  nchoicelem17  6306