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  6442  prarloclem5  6483  cauappcvgprlemlol  6619  cauappcvgprlemupu  6621  caucvgprlemlol  6641  caucvgprlemupu  6643  cnegexlem2  6984  apcotr  7391  apadd1  7392  mulext1  7396  div2negap  7493  ltdiv2  7634  nndivtr  7736  zdivmul  8106  gtndiv  8111  fzind  8129  eluzuzle  8257  eluzp1p1  8274  peano2uz  8302  qdivcl  8352  irrmul  8356  xrre2  8504  ubioc1  8568  ubicc2  8623  uzsubsubfz  8681  elfz1b  8722  fzp1nel  8736  fz0fzdiffz0  8757  difelfzle  8762  elfzo0  8808  elfzonlteqm1  8836  fzonn0p1p1  8839  fzosplitprm1  8860  fzoshftral  8864  expival  8911  redivap  9102  imdivap  9109