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  7215  frfi  9290  ressress  17195  funcestrcsetclem9  18102  funcsetcestrclem9  18117  latjjdir  18447  grprcan  18860  grpsubrcan  18906  grpaddsubass  18915  mhmmnd  18949  zntoslem  21118  ipdir  21198  ipass  21204  qustgpopn  23631  extwwlkfab  29643  grpomuldivass  29832  nvmdi  29939  dmdsl3  31606  dvrcan5  32426  imaslmod  32509  idlsrgmnd  32673  esum2d  33160  voliune  33296  btwnconn1lem7  35134  poimirlem4  36578  cvrnbtwn4  38235  paddasslem14  38790  paddasslem17  38793  paddss  38802  pmod1i  38805  cdleme1  39184  cdleme2  39185  xlimbr  44622  sbgoldbst  46525  funcringcsetcALTV2lem9  47021  funcringcsetclem9ALTV  47044