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  7154  frfi  9180  ressress  17165  funcestrcsetclem9  18062  funcsetcestrclem9  18077  latjjdir  18406  grprcan  18894  grpsubrcan  18942  grpaddsubass  18951  mhmmnd  18985  zntoslem  21502  ipdir  21585  ipass  21591  qustgpopn  24055  extwwlkfab  30353  grpomuldivass  30542  nvmdi  30649  dmdsl3  32316  dvrcan5  33246  imaslmod  33362  idlsrgmnd  33523  esum2d  34178  voliune  34314  btwnconn1lem7  36209  poimirlem4  37737  cvrnbtwn4  39451  paddasslem14  40005  paddasslem17  40008  paddss  40017  pmod1i  40020  cdleme1  40399  cdleme2  40400  xlimbr  45987  sbgoldbst  47940  funcringcsetcALTV2lem9  48460  funcringcsetclem9ALTV  48483