Theorem rgen3 3175

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2110  ∀wral 3045

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 3046

This theorem is referenced by:  poseq  8083  isposi  18221  efmndsgrp  18786  smndex1sgrp  18808  xrge0omnd  21375  addcnlem  24773  addscutlem  27913  zsoring  28325  isgrpoi  30468  lnocoi  30727  0lnfn  31955  lnopcoi  31973  reofld  33298  2zrngasgrp  48256  2zrngmsgrp  48263  2zrngALT  48264