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  7210  frfi  9255  ressress  17339  funcestrcsetclem9  18236  funcsetcestrclem9  18251  latjjdir  18580  grprcan  19097  grpsubrcan  19144  grpaddsubass  19153  mhmmnd  19187  zntoslem  21769  ipdir  21852  ipass  21858  qustgpopn  24346  extwwlkfab  30832  grpomuldivass  31022  nvmdi  31129  dmdsl3  32796  dvrcan5  33675  imaslmod  33793  idlsrgmnd  33924  esum2d  34603  voliune  34740  btwnconn1lem7  36673  poimirlem4  38373  cvrnbtwn4  40152  paddasslem14  40706  paddasslem17  40709  paddss  40718  pmod1i  40721  cdleme1  41100  cdleme2  41101  xlimbr  46655  sbgoldbst  48694  funcringcsetcALTV2lem9  49213  funcringcsetclem9ALTV  49236