Theorem 3ad2antr2 1187

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antr2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3ad2antr2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantrl 712	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1169	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

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

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 396  df-3an 1087

This theorem is referenced by:  simpr2  1193  simpr2l  1230  simpr2r  1231  simpr21  1258  simpr22  1259  simpr23  1260  wereu  5584  axdc4lem  10195  ioc0  13108  funcestrcsetclem9  17846  funcsetcestrclem9  17861  grpsubadd  18644  zntoslem  20745  psrbaglesuppOLD  21109  mdsl3  30657  dvrcan5  31469  idlsrgmnd  31638  prv1n  33372  brofs2  34358  brifs2  34359  poimirlem28  35784  ftc1anc  35837  frinfm  35872  welb  35873  fdc  35882  unichnidl  36168  cvrnbtwn2  37268  islpln2a  37541  paddss1  37810  paddss2  37811  paddasslem17  37829  tendospass  39012  funcringcsetcALTV2lem9  45554  funcringcsetclem9ALTV  45577  ldepsprlem  45765