Theorem 3ad2antr3 1190

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 714	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1169	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simpr3  1196  simpr3l  1234  simpr3r  1235  simpr31  1263  simpr32  1264  simpr33  1265  fpr2g  7212  frfi  9287  ressress  17192  funcestrcsetclem9  18099  funcsetcestrclem9  18114  latjjdir  18444  grprcan  18857  grpsubrcan  18903  grpaddsubass  18912  mhmmnd  18946  zntoslem  21111  ipdir  21191  ipass  21197  qustgpopn  23623  extwwlkfab  29602  grpomuldivass  29789  nvmdi  29896  dmdsl3  31563  dvrcan5  32380  imaslmod  32463  idlsrgmnd  32623  esum2d  33086  voliune  33222  btwnconn1lem7  35060  poimirlem4  36487  cvrnbtwn4  38144  paddasslem14  38699  paddasslem17  38702  paddss  38711  pmod1i  38714  cdleme1  39093  cdleme2  39094  xlimbr  44533  sbgoldbst  46436  funcringcsetcALTV2lem9  46932  funcringcsetclem9ALTV  46955