Theorem rgen3 3179

Description: Generalization rule for restricted quantification, with three quantifiers. (Contributed by NM, 12-Jan-2008.)

Hypothesis

Ref	Expression
rgen3.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)

Assertion

Ref	Expression
rgen3	⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑

Distinct variable groups:   𝑦,𝑧,𝐴   𝑧,𝐵   𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝐴(𝑥)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦,𝑧)

Proof of Theorem rgen3

Step	Hyp	Ref	Expression
1		rgen3.1	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)
2	1	3expa 1118	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜑)
3	2	ralrimiva 3126	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜑)
4	3	rgen2 3174	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2113  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ral 3050

This theorem is referenced by:  poseq  8098  isposi  18244  efmndsgrp  18809  smndex1sgrp  18831  xrge0omnd  21398  addcnlem  24807  addscutlem  27947  zsoring  28367  isgrpoi  30522  lnocoi  30781  0lnfn  32009  lnopcoi  32027  reofld  33373  2zrngasgrp  48434  2zrngmsgrp  48441  2zrngALT  48442