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 1087

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 1089

This theorem is referenced by:  simpr3  1197  simpr3l  1235  simpr3r  1236  simpr31  1264  simpr32  1265  simpr33  1266  fpr2g  7231  frfi  9321  ressress  17293  funcestrcsetclem9  18193  funcsetcestrclem9  18208  latjjdir  18537  grprcan  18991  grpsubrcan  19039  grpaddsubass  19048  mhmmnd  19082  zntoslem  21575  ipdir  21657  ipass  21663  qustgpopn  24128  extwwlkfab  30371  grpomuldivass  30560  nvmdi  30667  dmdsl3  32334  dvrcan5  33240  imaslmod  33381  idlsrgmnd  33542  esum2d  34094  voliune  34230  btwnconn1lem7  36094  poimirlem4  37631  cvrnbtwn4  39280  paddasslem14  39835  paddasslem17  39838  paddss  39847  pmod1i  39850  cdleme1  40229  cdleme2  40230  xlimbr  45842  sbgoldbst  47765  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237