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  5620  axdc4lem  10365  ioc0  13308  funcestrcsetclem9  18071  funcsetcestrclem9  18086  grpsubadd  18958  zntoslem  21511  mdsl3  32391  dvrcan5  33318  idlsrgmnd  33595  prv1n  35625  brofs2  36271  brifs2  36272  poimirlem28  37849  ftc1anc  37902  frinfm  37936  welb  37937  fdc  37946  unichnidl  38232  cvrnbtwn2  39535  islpln2a  39808  paddss1  40077  paddss2  40078  paddasslem17  40096  tendospass  41279  funcringcsetcALTV2lem9  48544  funcringcsetclem9ALTV  48567  ldepsprlem  48718