Theorem 3ad2ant2 925

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

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (φ → χ)

Assertion

Ref	Expression
3ad2ant2	⊢ ((ψ ∧ φ ∧ θ) → χ)

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (φ → χ)
2	1	adantr 261	. 2 ⊢ ((φ ∧ θ) → χ)
3	2	3adant1 921	1 ⊢ ((ψ ∧ φ ∧ θ) → χ)

Syntax hints:   → wi 4   ∧ w3a 884

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 886

This theorem is referenced by:  simp2l  929  simp2r  930  simp21  936  simp22  937  simp23  938  simp2ll  970  simp2lr  971  simp2rl  972  simp2rr  973  simp2l1  1002  simp2l2  1003  simp2l3  1004  simp2r1  1005  simp2r2  1006  simp2r3  1007  simp21l  1020  simp21r  1021  simp22l  1022  simp22r  1023  simp23l  1024  simp23r  1025  simp211  1041  simp212  1042  simp213  1043  simp221  1044  simp222  1045  simp223  1046  simp231  1047  simp232  1048  simp233  1049  3anim123i  1088  3jaao  1202  ceqsalt  2574  vtoclgft  2598  vtoclegft  2619  elirr  4224  en2lp  4232  sotri3  4666  funtpg  4893  fnprg  4897  fntpg  4898  funimaexglem  4925  fnco  4950  fvun1  5182  oprssov  5584  caovimo  5636  rdgivallem  5908  f1dom2g  6172  distrnqg  6371  distrnq0  6441  prarloclem5  6482  cauappcvgprlemlol  6618  cauappcvgprlemupu  6620  cnegexlem2  6964  apcotr  7371  apadd1  7372  mulext1  7376  div2negap  7473  ltdiv2  7614  nndivtr  7716  zdivmul  8086  gtndiv  8091  fzind  8109  eluzuzle  8237  eluzp1p1  8254  peano2uz  8282  qdivcl  8332  irrmul  8336  xrre2  8484  ubioc1  8548  ubicc2  8603  uzsubsubfz  8661  elfz1b  8702  fzp1nel  8716  fz0fzdiffz0  8737  difelfzle  8742  elfzo0  8788  elfzonlteqm1  8816  fzonn0p1p1  8819  fzosplitprm1  8840  fzoshftral  8844  expival  8891  redivap  9082  imdivap  9089