Theorem rgen3 3184

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 1124	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜑)
3	2	ralrimiva 3131	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜑)
4	3	rgen2 3179	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-ral 3054

This theorem is referenced by:  poseq  8098  isposi  18280  efmndsgrp  18845  smndex1sgrp  18870  xrge0omnd  21420  addcnlem  24848  addcutslem  27987  zsoring  28419  isgrpoi  30587  lnocoi  30846  0lnfn  32074  lnopcoi  32092  reofld  33426  2zrngasgrp  48737  2zrngmsgrp  48744  2zrngALT  48745