Theorem 3ad2antr3 1189

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 1168	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  1195  simpr3l  1233  simpr3r  1234  simpr31  1262  simpr32  1263  simpr33  1264  fpr2g  7231  frfi  9319  ressress  17294  funcestrcsetclem9  18204  funcsetcestrclem9  18219  latjjdir  18550  grprcan  19004  grpsubrcan  19052  grpaddsubass  19061  mhmmnd  19095  zntoslem  21593  ipdir  21675  ipass  21681  qustgpopn  24144  extwwlkfab  30381  grpomuldivass  30570  nvmdi  30677  dmdsl3  32344  dvrcan5  33226  imaslmod  33361  idlsrgmnd  33522  esum2d  34074  voliune  34210  btwnconn1lem7  36075  poimirlem4  37611  cvrnbtwn4  39261  paddasslem14  39816  paddasslem17  39819  paddss  39828  pmod1i  39831  cdleme1  40210  cdleme2  40211  xlimbr  45783  sbgoldbst  47703  funcringcsetcALTV2lem9  48142  funcringcsetclem9ALTV  48165