ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralrimivvva GIF version

Theorem ralrimivvva 2573
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.)
Hypothesis
Ref Expression
ralrimivvva.1 ((𝜑 ∧ (𝑥𝐴𝑦𝐵𝑧𝐶)) → 𝜓)
Assertion
Ref Expression
ralrimivvva (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Distinct variable groups:   𝜑,𝑥,𝑦,𝑧   𝑦,𝐴,𝑧   𝑧,𝐵
Allowed substitution hints:   𝜓(𝑥,𝑦,𝑧)   𝐴(𝑥)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦,𝑧)

Proof of Theorem ralrimivvva
StepHypRef Expression
1 ralrimivvva.1 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵𝑧𝐶)) → 𝜓)
213anassrs 1231 . . . 4 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝑧𝐶) → 𝜓)
32ralrimiva 2563 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 2563 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 2563 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 980  wcel 2160  wral 2468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537
This theorem depends on definitions:  df-bi 117  df-3an 982  df-nf 1472  df-ral 2473
This theorem is referenced by:  ispod  4322  swopolem  4323  ordwe  4593  wessep  4595  isopolem  5844  caovassg  6056  caovcang  6059  caovordig  6063  caovordg  6065  caovdig  6072  caovdirg  6075  caoftrn  6133  netap  7284  2omotaplemap  7287  isrngd  13324  isringd  13412  aprap  13619  islmodd  13626  rnglidlmsgrp  13830  rnglidlrng  13831
  Copyright terms: Public domain W3C validator