Theorem 3ad2antr3 1191

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpr3  1197  simpr3l  1235  simpr3r  1236  simpr31  1264  simpr32  1265  simpr33  1266  fpr2g  7157  frfi  9185  ressress  17174  funcestrcsetclem9  18071  funcsetcestrclem9  18086  latjjdir  18415  grprcan  18903  grpsubrcan  18951  grpaddsubass  18960  mhmmnd  18994  zntoslem  21511  ipdir  21594  ipass  21600  qustgpopn  24064  extwwlkfab  30427  grpomuldivass  30616  nvmdi  30723  dmdsl3  32390  dvrcan5  33318  imaslmod  33434  idlsrgmnd  33595  esum2d  34250  voliune  34386  btwnconn1lem7  36287  poimirlem4  37825  cvrnbtwn4  39539  paddasslem14  40093  paddasslem17  40096  paddss  40105  pmod1i  40108  cdleme1  40487  cdleme2  40488  xlimbr  46071  sbgoldbst  48024  funcringcsetcALTV2lem9  48544  funcringcsetclem9ALTV  48567