Theorem 3ad2antl1 1190

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 481	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl2 1185	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  acexmid  6087  f1oen4g  7044  f1dom4g  7045  ordiso2  7381  addlocpr  7909  distrlem1prl  7955  distrlem1pru  7956  ltsopr  7969  addcanprlemu  7988  fzo1fzo0n0  10611  pfxsuffeqwrdeq  11491  prodfap0  12336  prodfrecap  12337  muldvds2  12608  dvds2add  12616  dvds2sub  12617  dvdstr  12619  qusaddvallemg  13712  mulgnnsubcl  13995  mulgpropdg  14025  ringidss  14440  lmodprop2d  14793  issubassa  15121  cnpnei  15462  upxp  15515  lgsval4lem  16352  clwwlkccatlem  16863  clwwlkccat  16864