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

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

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 1105

This theorem is referenced by:  simpr3  1215  simpr3l  1253  simpr3r  1254  simpr31  1282  simpr32  1283  simpr33  1284  fpr2g  7209  frfi  9241  ressress  17302  funcestrcsetclem9  18199  funcsetcestrclem9  18214  latjjdir  18543  grprcan  19035  grpsubrcan  19082  grpaddsubass  19091  mhmmnd  19125  zntoslem  21706  ipdir  21789  ipass  21795  qustgpopn  24277  extwwlkfab  30703  grpomuldivass  30893  nvmdi  31000  dmdsl3  32667  dvrcan5  33555  imaslmod  33673  idlsrgmnd  33804  esum2d  34483  voliune  34619  btwnconn1lem7  36585  poimirlem4  38275  cvrnbtwn4  40053  paddasslem14  40607  paddasslem17  40610  paddss  40619  pmod1i  40622  cdleme1  41001  cdleme2  41002  xlimbr  46541  sbgoldbst  48543  funcringcsetcALTV2lem9  49063  funcringcsetclem9ALTV  49086