Theorem 3ad2antr3 1197

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpr3  1203  simpr3l  1241  simpr3r  1242  simpr31  1270  simpr32  1271  simpr33  1272  fpr2g  7155  frfi  9185  ressress  17208  funcestrcsetclem9  18105  funcsetcestrclem9  18120  latjjdir  18449  grprcan  18940  grpsubrcan  18988  grpaddsubass  18997  mhmmnd  19031  zntoslem  21531  ipdir  21614  ipass  21620  qustgpopn  24103  extwwlkfab  30440  grpomuldivass  30630  nvmdi  30737  dmdsl3  32404  dvrcan5  33317  imaslmod  33436  idlsrgmnd  33597  esum2d  34277  voliune  34413  btwnconn1lem7  36321  poimirlem4  37991  cvrnbtwn4  39771  paddasslem14  40325  paddasslem17  40328  paddss  40337  pmod1i  40340  cdleme1  40719  cdleme2  40720  xlimbr  46270  sbgoldbst  48269  funcringcsetcALTV2lem9  48789  funcringcsetclem9ALTV  48812