Theorem 3ad2antr3 1189

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpr3  1195  simpr3l  1233  simpr3r  1234  simpr31  1262  simpr32  1263  simpr33  1264  fpr2g  7087  frfi  9059  ressress  16958  funcestrcsetclem9  17865  funcsetcestrclem9  17880  latjjdir  18210  grprcan  18613  grpsubrcan  18656  grpaddsubass  18665  mhmmnd  18697  zntoslem  20764  ipdir  20844  ipass  20850  qustgpopn  23271  extwwlkfab  28716  grpomuldivass  28903  nvmdi  29010  dmdsl3  30677  dvrcan5  31490  imaslmod  31553  idlsrgmnd  31659  esum2d  32061  voliune  32197  btwnconn1lem7  34395  poimirlem4  35781  cvrnbtwn4  37293  paddasslem14  37847  paddasslem17  37850  paddss  37859  pmod1i  37862  cdleme1  38241  cdleme2  38242  xlimbr  43368  sbgoldbst  45230  funcringcsetcALTV2lem9  45602  funcringcsetclem9ALTV  45625