Theorem 3ad2antr3 1221

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antr3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3ad2antr3

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantrl 748	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1213	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  fpr2g  6380  frfi  8090  ressress  15765  funcestrcsetclem9  16611  funcsetcestrclem9  16626  latjjdir  16927  grprcan  17278  grpsubrcan  17319  grpaddsubass  17328  mhmmnd  17360  zntoslem  19724  ipdir  19803  ipass  19809  qustgpopn  21733  constr3trllem1  26178  wwlkextproplem3  26271  grpomuldivass  26779  nvmdi  26887  dmdsl3  28558  dvrcan5  29124  esum2d  29482  voliune  29619  btwnconn1lem7  31370  poimirlem4  32583  cvrnbtwn4  33584  paddasslem14  34137  paddasslem17  34140  paddss  34149  pmod1i  34152  cdleme1  34532  cdleme2  34533  bgoldbst  40200  funcringcsetcALTV2lem9  41836  funcringcsetclem9ALTV  41859