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  7248  frfi  9314  ressress  17469  funcestrcsetclem9  18372  funcsetcestrclem9  18387  latjjdir  18716  grprcan  19234  grpsubrcan  19281  grpaddsubass  19290  mhmmnd  19324  zntoslem  21917  ipdir  22000  ipass  22006  qustgpopn  24494  extwwlkfab  31010  grpomuldivass  31200  nvmdi  31307  dmdsl3  32974  dvrcan5  33895  imaslmod  34018  idlsrgmnd  34150  esum2d  34836  voliune  34973  btwnconn1lem7  37073  poimirlem4  38810  cvrnbtwn4  40602  paddasslem14  41156  paddasslem17  41159  paddss  41168  pmod1i  41171  cdleme1  41550  cdleme2  41551  xlimbr  47110  sbgoldbst  49149  funcringcsetcALTV2lem9  49668  funcringcsetclem9ALTV  49691