Theorem 3ad2antr3 1186

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 1165	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpr3  1192  simpr3l  1230  simpr3r  1231  simpr31  1259  simpr32  1260  simpr33  1261  fpr2g  6968  frfi  8757  ressress  16556  funcestrcsetclem9  17392  funcsetcestrclem9  17407  latjjdir  17708  grprcan  18131  grpsubrcan  18174  grpaddsubass  18183  mhmmnd  18215  zntoslem  20697  ipdir  20777  ipass  20783  qustgpopn  22722  extwwlkfab  28125  grpomuldivass  28312  nvmdi  28419  dmdsl3  30086  dvrcan5  30859  imaslmod  30917  esum2d  31347  voliune  31483  btwnconn1lem7  33549  poimirlem4  34890  cvrnbtwn4  36409  paddasslem14  36963  paddasslem17  36966  paddss  36975  pmod1i  36978  cdleme1  37357  cdleme2  37358  xlimbr  42101  sbgoldbst  43937  funcringcsetcALTV2lem9  44309  funcringcsetclem9ALTV  44332