Theorem 3ad2antr3 1220

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  fpr2g  6357  frfi  8067  ressress  15713  funcestrcsetclem9  16559  funcsetcestrclem9  16574  latjjdir  16875  grprcan  17226  grpsubrcan  17267  grpaddsubass  17276  mhmmnd  17308  zntoslem  19671  ipdir  19750  ipass  19756  qustgpopn  21680  constr3trllem1  25971  wwlkextproplem3  26064  grpomuldivass  26572  nvmdi  26680  dmdsl3  28351  dvrcan5  28917  esum2d  29275  voliune  29412  btwnconn1lem7  31163  poimirlem4  32366  cvrnbtwn4  33367  paddasslem14  33920  paddasslem17  33923  paddss  33932  pmod1i  33935  cdleme1  34315  cdleme2  34316  bgoldbst  39984  funcringcsetcALTV2lem9  41817  funcringcsetclem9ALTV  41840