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  7216  frfi  9252  ressress  17329  funcestrcsetclem9  18226  funcsetcestrclem9  18241  latjjdir  18570  grprcan  19084  grpsubrcan  19131  grpaddsubass  19140  mhmmnd  19174  zntoslem  21756  ipdir  21839  ipass  21845  qustgpopn  24328  extwwlkfab  30774  grpomuldivass  30964  nvmdi  31071  dmdsl3  32738  dvrcan5  33619  imaslmod  33737  idlsrgmnd  33868  esum2d  34547  voliune  34684  btwnconn1lem7  36622  poimirlem4  38332  cvrnbtwn4  40111  paddasslem14  40665  paddasslem17  40668  paddss  40677  pmod1i  40680  cdleme1  41059  cdleme2  41060  xlimbr  46599  sbgoldbst  48601  funcringcsetcALTV2lem9  49120  funcringcsetclem9ALTV  49143