Theorem 3ad2antr3 1228

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 752	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1220	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  fpr2g  6475  frfi  8205  ressress  15938  funcestrcsetclem9  16788  funcsetcestrclem9  16803  latjjdir  17104  grprcan  17455  grpsubrcan  17496  grpaddsubass  17505  mhmmnd  17537  zntoslem  19905  ipdir  19984  ipass  19990  qustgpopn  21923  grpomuldivass  27395  nvmdi  27503  dmdsl3  29174  dvrcan5  29793  esum2d  30155  voliune  30292  btwnconn1lem7  32200  poimirlem4  33413  cvrnbtwn4  34566  paddasslem14  35119  paddasslem17  35122  paddss  35131  pmod1i  35134  cdleme1  35514  cdleme2  35515  xlimbr  40053  sbgoldbst  41666  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067