Theorem 3ad2antl1 1183

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

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

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 1004

This theorem is referenced by:  acexmid  5999  f1oen4g  6901  f1dom4g  6902  ordiso2  7198  addlocpr  7719  distrlem1prl  7765  distrlem1pru  7766  ltsopr  7779  addcanprlemu  7798  fzo1fzo0n0  10379  pfxsuffeqwrdeq  11225  prodfap0  12051  prodfrecap  12052  muldvds2  12323  dvds2add  12331  dvds2sub  12332  dvdstr  12334  qusaddvallemg  13361  mulgnnsubcl  13666  mulgpropdg  13696  ringidss  13987  lmodprop2d  14306  cnpnei  14887  upxp  14940  lgsval4lem  15684