Theorem 3ad2antr2 1190

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 716	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1172	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:  simpr2  1196  simpr2l  1233  simpr2r  1234  simpr21  1261  simpr22  1262  simpr23  1263  wereu  5610  axdc4lem  10346  ioc0  13292  funcestrcsetclem9  18054  funcsetcestrclem9  18069  grpsubadd  18941  zntoslem  21493  mdsl3  32296  dvrcan5  33203  idlsrgmnd  33479  prv1n  35475  brofs2  36121  brifs2  36122  poimirlem28  37698  ftc1anc  37751  frinfm  37785  welb  37786  fdc  37795  unichnidl  38081  cvrnbtwn2  39384  islpln2a  39657  paddss1  39926  paddss2  39927  paddasslem17  39945  tendospass  41128  funcringcsetcALTV2lem9  48408  funcringcsetclem9ALTV  48431  ldepsprlem  48583