Theorem 3ad2antl1 1162

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antl1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3ad2antl1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantlr 477	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1157	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  acexmid  5943  f1oen4g  6843  f1dom4g  6844  ordiso2  7137  addlocpr  7649  distrlem1prl  7695  distrlem1pru  7696  ltsopr  7709  addcanprlemu  7728  fzo1fzo0n0  10307  prodfap0  11856  prodfrecap  11857  muldvds2  12128  dvds2add  12136  dvds2sub  12137  dvdstr  12139  qusaddvallemg  13165  mulgnnsubcl  13470  mulgpropdg  13500  ringidss  13791  lmodprop2d  14110  cnpnei  14691  upxp  14744  lgsval4lem  15488