Theorem 3ad2antr3 1206

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  simpr3  1238  simpr3l  1299  simpr3r  1301  simpr31  1345  simpr32  1347  simpr33  1349  fpr2g  6640  frfi  8372  ressress  16160  funcestrcsetclem9  17009  funcsetcestrclem9  17024  latjjdir  17325  grprcan  17676  grpsubrcan  17717  grpaddsubass  17726  mhmmnd  17758  zntoslem  20127  ipdir  20206  ipass  20212  qustgpopn  22144  extwwlkfab  27532  grpomuldivass  27725  nvmdi  27833  dmdsl3  29504  dvrcan5  30123  esum2d  30485  voliune  30622  btwnconn1lem7  32527  poimirlem4  33744  cvrnbtwn4  35087  paddasslem14  35640  paddasslem17  35643  paddss  35652  pmod1i  35655  cdleme1  36035  cdleme2  36036  xlimbr  40574  sbgoldbst  42194  funcringcsetcALTV2lem9  42572  funcringcsetclem9ALTV  42595