Theorem 3ad2antr3 1209

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr3  1215  simpr3l  1253  simpr3r  1254  simpr31  1282  simpr32  1283  simpr33  1284  fpr2g  7221  frfi  9283  ressress  17434  funcestrcsetclem9  18331  funcsetcestrclem9  18346  latjjdir  18675  grprcan  19193  grpsubrcan  19240  grpaddsubass  19249  mhmmnd  19283  zntoslem  21871  ipdir  21954  ipass  21960  qustgpopn  24448  extwwlkfab  30962  grpomuldivass  31152  nvmdi  31259  dmdsl3  32926  dvrcan5  33846  imaslmod  33964  idlsrgmnd  34096  esum2d  34775  voliune  34912  btwnconn1lem7  36954  poimirlem4  38651  cvrnbtwn4  40445  paddasslem14  40999  paddasslem17  41002  paddss  41011  pmod1i  41014  cdleme1  41393  cdleme2  41394  xlimbr  46945  sbgoldbst  48984  funcringcsetcALTV2lem9  49503  funcringcsetclem9ALTV  49526