Theorem 3ad2antr3 1207

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpr3  1213  simpr3l  1251  simpr3r  1252  simpr31  1280  simpr32  1281  simpr33  1282  fpr2g  7210  frfi  9244  ressress  17306  funcestrcsetclem9  18203  funcsetcestrclem9  18218  latjjdir  18547  grprcan  19039  grpsubrcan  19086  grpaddsubass  19095  mhmmnd  19129  zntoslem  21674  ipdir  21757  ipass  21763  qustgpopn  24245  extwwlkfab  30643  grpomuldivass  30833  nvmdi  30940  dmdsl3  32607  dvrcan5  33495  imaslmod  33615  idlsrgmnd  33748  esum2d  34427  voliune  34563  btwnconn1lem7  36483  poimirlem4  38162  cvrnbtwn4  39942  paddasslem14  40496  paddasslem17  40499  paddss  40508  pmod1i  40511  cdleme1  40890  cdleme2  40891  xlimbr  46432  sbgoldbst  48431  funcringcsetcALTV2lem9  48951  funcringcsetclem9ALTV  48974