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  7140  frfi  9164  ressress  17153  funcestrcsetclem9  18049  funcsetcestrclem9  18064  latjjdir  18393  grprcan  18881  grpsubrcan  18929  grpaddsubass  18938  mhmmnd  18972  zntoslem  21488  ipdir  21571  ipass  21577  qustgpopn  24030  extwwlkfab  30324  grpomuldivass  30513  nvmdi  30620  dmdsl3  32287  dvrcan5  33195  imaslmod  33310  idlsrgmnd  33471  esum2d  34098  voliune  34234  btwnconn1lem7  36127  poimirlem4  37664  cvrnbtwn4  39318  paddasslem14  39872  paddasslem17  39875  paddss  39884  pmod1i  39887  cdleme1  40266  cdleme2  40267  xlimbr  45865  sbgoldbst  47809  funcringcsetcALTV2lem9  48329  funcringcsetclem9ALTV  48352