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-1 5  ax-2 6  ax-3 7  ax-mp 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  2881  sbciegft  3076  reupick2  3541  otkelins2kg  4253  otkelins3kg  4254  nnsucelrlem3  4426  ssfin  4470  ncfinlower  4483  tfin11  4493  nnpweq  4523  sfinltfin  4535  vfintle  4546  vfinncvntnn  4548  peano4  4557  funprg  5149  funprgOLD  5150  fvun1  5379  fvopab4t  5385  po0  5939  nenpw1pwlem2  6085  ceclnn1  6189  nclenc  6222  lenc  6223  taddc  6229  letc  6231  nclenn  6249  addcdi  6250  spaccl  6286  nchoicelem17  6305