Theorem 3ad2antl1 1161

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 1156	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

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

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 982

This theorem is referenced by:  acexmid  5942  f1oen4g  6842  f1dom4g  6843  ordiso2  7136  addlocpr  7648  distrlem1prl  7694  distrlem1pru  7695  ltsopr  7708  addcanprlemu  7727  fzo1fzo0n0  10305  prodfap0  11827  prodfrecap  11828  muldvds2  12099  dvds2add  12107  dvds2sub  12108  dvdstr  12110  qusaddvallemg  13136  mulgnnsubcl  13441  mulgpropdg  13471  ringidss  13762  lmodprop2d  14081  cnpnei  14662  upxp  14715  lgsval4lem  15459