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 715	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1169	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  1196  simpr3l  1234  simpr3r  1235  simpr31  1263  simpr32  1264  simpr33  1265  fpr2g  7248  frfi  9349  ressress  17307  funcestrcsetclem9  18217  funcsetcestrclem9  18232  latjjdir  18562  grprcan  19013  grpsubrcan  19061  grpaddsubass  19070  mhmmnd  19104  zntoslem  21598  ipdir  21680  ipass  21686  qustgpopn  24149  extwwlkfab  30384  grpomuldivass  30573  nvmdi  30680  dmdsl3  32347  dvrcan5  33216  imaslmod  33346  idlsrgmnd  33507  esum2d  34057  voliune  34193  btwnconn1lem7  36057  poimirlem4  37584  cvrnbtwn4  39235  paddasslem14  39790  paddasslem17  39793  paddss  39802  pmod1i  39805  cdleme1  40184  cdleme2  40185  xlimbr  45748  sbgoldbst  47652  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044