Theorem 3ad2antr3 1191

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  simpr3  1197  simpr3l  1235  simpr3r  1236  simpr31  1264  simpr32  1265  simpr33  1266  fpr2g  7208  frfi  9298  ressress  17273  funcestrcsetclem9  18165  funcsetcestrclem9  18180  latjjdir  18507  grprcan  18961  grpsubrcan  19009  grpaddsubass  19018  mhmmnd  19052  zntoslem  21522  ipdir  21604  ipass  21610  qustgpopn  24063  extwwlkfab  30338  grpomuldivass  30527  nvmdi  30634  dmdsl3  32301  dvrcan5  33236  imaslmod  33373  idlsrgmnd  33534  esum2d  34129  voliune  34265  btwnconn1lem7  36116  poimirlem4  37653  cvrnbtwn4  39302  paddasslem14  39857  paddasslem17  39860  paddss  39869  pmod1i  39872  cdleme1  40251  cdleme2  40252  xlimbr  45823  sbgoldbst  47759  funcringcsetcALTV2lem9  48240  funcringcsetclem9ALTV  48263