Theorem 3ad2antr3 1192

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 717	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1171	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  1198  simpr3l  1236  simpr3r  1237  simpr31  1265  simpr32  1266  simpr33  1267  fpr2g  7167  frfi  9197  ressress  17186  funcestrcsetclem9  18083  funcsetcestrclem9  18098  latjjdir  18427  grprcan  18915  grpsubrcan  18963  grpaddsubass  18972  mhmmnd  19006  zntoslem  21523  ipdir  21606  ipass  21612  qustgpopn  24076  extwwlkfab  30439  grpomuldivass  30629  nvmdi  30736  dmdsl3  32403  dvrcan5  33330  imaslmod  33446  idlsrgmnd  33607  esum2d  34271  voliune  34407  btwnconn1lem7  36309  poimirlem4  37875  cvrnbtwn4  39655  paddasslem14  40209  paddasslem17  40212  paddss  40221  pmod1i  40224  cdleme1  40603  cdleme2  40604  xlimbr  46185  sbgoldbst  48138  funcringcsetcALTV2lem9  48658  funcringcsetclem9ALTV  48681