Theorem 3ad2ant2 977

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- (ph -> ch)
2	1	adantr 451	. 2 |- ((ph /\ th) -> ch)
3	2	3adant1 973	1 |- ((ps /\ ph /\ 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:  simp2l  981  simp2r  982  simp21  988  simp22  989  simp23  990  simp2ll  1022  simp2lr  1023  simp2rl  1024  simp2rr  1025  simp2l1  1054  simp2l2  1055  simp2l3  1056  simp2r1  1057  simp2r2  1058  simp2r3  1059  simp21l  1072  simp21r  1073  simp22l  1074  simp22r  1075  simp23l  1076  simp23r  1077  simp211  1093  simp212  1094  simp213  1095  simp221  1096  simp222  1097  simp223  1098  simp231  1099  simp232  1100  simp233  1101  3anim123i  1137  3jaao  1249  ceqsalt  2881  vtoclgft  2905  vtoclegft  2926  cokrelk  4284  ssfin  4470  ncfinlower  4483  tfin11  4493  funprg  5149  fnco  5191  fvun1  5379  oprssov  5603  po0  5939  connex0  5940  enadj  6060  enprmaplem5  6080  nclenc  6222  lenc  6223  letc  6231  spaccl  6286