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-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:  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  2882  vtoclgft  2906  vtoclegft  2927  cokrelk  4285  ssfin  4471  ncfinlower  4484  tfin11  4494  funprg  5150  fnco  5192  fvun1  5380  oprssov  5604  po0  5940  connex0  5941  enadj  6061  enprmaplem5  6081  nclenc  6223  lenc  6224  letc  6232  spaccl  6287