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  7167  frfi  9208  ressress  17193  funcestrcsetclem9  18085  funcsetcestrclem9  18100  latjjdir  18427  grprcan  18881  grpsubrcan  18929  grpaddsubass  18938  mhmmnd  18972  zntoslem  21442  ipdir  21524  ipass  21530  qustgpopn  23983  extwwlkfab  30254  grpomuldivass  30443  nvmdi  30550  dmdsl3  32217  dvrcan5  33160  imaslmod  33297  idlsrgmnd  33458  esum2d  34056  voliune  34192  btwnconn1lem7  36054  poimirlem4  37591  cvrnbtwn4  39245  paddasslem14  39800  paddasslem17  39803  paddss  39812  pmod1i  39815  cdleme1  40194  cdleme2  40195  xlimbr  45798  sbgoldbst  47752  funcringcsetcALTV2lem9  48259  funcringcsetclem9ALTV  48282