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 1087

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 1089

This theorem is referenced by:  simpr2  1196  simpr2l  1233  simpr2r  1234  simpr21  1261  simpr22  1262  simpr23  1263  wereu  5681  axdc4lem  10495  ioc0  13434  funcestrcsetclem9  18193  funcsetcestrclem9  18208  grpsubadd  19046  zntoslem  21575  mdsl3  32335  dvrcan5  33240  idlsrgmnd  33542  prv1n  35436  brofs2  36078  brifs2  36079  poimirlem28  37655  ftc1anc  37708  frinfm  37742  welb  37743  fdc  37752  unichnidl  38038  cvrnbtwn2  39276  islpln2a  39550  paddss1  39819  paddss2  39820  paddasslem17  39838  tendospass  41021  funcringcsetcALTV2lem9  48214  funcringcsetclem9ALTV  48237  ldepsprlem  48389