Theorem 3ad2antl1 1185

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

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

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 1006

This theorem is referenced by:  acexmid  6016  f1oen4g  6924  f1dom4g  6925  ordiso2  7233  addlocpr  7755  distrlem1prl  7801  distrlem1pru  7802  ltsopr  7815  addcanprlemu  7834  fzo1fzo0n0  10421  pfxsuffeqwrdeq  11278  prodfap0  12105  prodfrecap  12106  muldvds2  12377  dvds2add  12385  dvds2sub  12386  dvdstr  12388  qusaddvallemg  13415  mulgnnsubcl  13720  mulgpropdg  13750  ringidss  14041  lmodprop2d  14361  cnpnei  14942  upxp  14995  lgsval4lem  15739  clwwlkccatlem  16250  clwwlkccat  16251