Theorem 3ad2antl1 1159

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

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

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 980

This theorem is referenced by:  acexmid  5873  ordiso2  7033  addlocpr  7534  distrlem1prl  7580  distrlem1pru  7581  ltsopr  7594  addcanprlemu  7613  fzo1fzo0n0  10182  prodfap0  11552  prodfrecap  11553  muldvds2  11823  dvds2add  11831  dvds2sub  11832  dvdstr  11834  qusaddvallemg  12751  mulgnnsubcl  12994  mulgpropdg  13023  ringidss  13210  cnpnei  13689  upxp  13742  lgsval4lem  14382