Theorem 3ad2antr3 1204

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  simpr3  1210  simpr3l  1248  simpr3r  1249  simpr31  1277  simpr32  1278  simpr33  1279  fpr2g  7195  frfi  9229  ressress  17283  funcestrcsetclem9  18180  funcsetcestrclem9  18195  latjjdir  18524  grprcan  19015  grpsubrcan  19063  grpaddsubass  19072  mhmmnd  19106  zntoslem  21605  ipdir  21688  ipass  21694  qustgpopn  24177  extwwlkfab  30551  grpomuldivass  30741  nvmdi  30848  dmdsl3  32515  dvrcan5  33413  imaslmod  33536  idlsrgmnd  33707  esum2d  34387  voliune  34523  btwnconn1lem7  36440  poimirlem4  38120  cvrnbtwn4  39900  paddasslem14  40454  paddasslem17  40457  paddss  40466  pmod1i  40469  cdleme1  40848  cdleme2  40849  xlimbr  46398  sbgoldbst  48397  funcringcsetcALTV2lem9  48917  funcringcsetclem9ALTV  48940