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  7215  frfi  9269  ressress  17418  funcestrcsetclem9  18315  funcsetcestrclem9  18330  latjjdir  18659  grprcan  19177  grpsubrcan  19224  grpaddsubass  19233  mhmmnd  19267  zntoslem  21855  ipdir  21938  ipass  21944  qustgpopn  24432  extwwlkfab  30946  grpomuldivass  31136  nvmdi  31243  dmdsl3  32910  dvrcan5  33789  imaslmod  33907  idlsrgmnd  34039  esum2d  34718  voliune  34855  btwnconn1lem7  36838  poimirlem4  38522  cvrnbtwn4  40316  paddasslem14  40870  paddasslem17  40873  paddss  40882  pmod1i  40885  cdleme1  41264  cdleme2  41265  xlimbr  46806  sbgoldbst  48845  funcringcsetcALTV2lem9  49364  funcringcsetclem9ALTV  49387