MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rgen3 Structured version   Visualization version   GIF version

Theorem rgen3 3198
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
StepHypRef Expression
1 rgen3.1 . . . 4 ((𝑥𝐴𝑦𝐵𝑧𝐶) → 𝜑)
213expa 1116 . . 3 (((𝑥𝐴𝑦𝐵) ∧ 𝑧𝐶) → 𝜑)
32ralrimiva 3142 . 2 ((𝑥𝐴𝑦𝐵) → ∀𝑧𝐶 𝜑)
43rgen2 3193 1 𝑥𝐴𝑦𝐵𝑧𝐶 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085  wcel 2099  wral 3057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-ral 3058
This theorem is referenced by:  poseq  8158  isposi  18310  efmndsgrp  18832  smndex1sgrp  18854  addcnlem  24774  addscutlem  27888  isgrpoi  30302  lnocoi  30561  0lnfn  31789  lnopcoi  31807  xrge0omnd  32786  reofld  33051  2zrngasgrp  47299  2zrngmsgrp  47306  2zrngALT  47307
  Copyright terms: Public domain W3C validator