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

Theorem alrimivv 1886
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
alrimivv.1 (𝜑𝜓)
Assertion
Ref Expression
alrimivv (𝜑 → ∀𝑥𝑦𝜓)
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem alrimivv
StepHypRef Expression
1 alrimivv.1 . . 3 (𝜑𝜓)
21alrimiv 1885 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1885 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1458  ax-gen 1460  ax-17 1537
This theorem is referenced by:  2ax17  1889  euind  2939  sbnfc2  3132  exmidsssn  4217  exmidel  4220  exmidundif  4221  exmidundifim  4222  ssopab2dv  4293  suctr  4436  eusvnf  4468  ordsuc  4577  ssrel  4729  relssdv  4733  eqrelrdv  4737  eqbrrdv  4738  eqrelrdv2  4740  ssrelrel  4741  iss  4968  funssres  5273  funun  5275  fununi  5299  fsn  5704  ovg  6030  caovimo  6085  oprabexd  6146  qliftfund  6636  eroveu  6644  th3qlem1  6655  exmidfodomrlemim  7218  exmidmotap  7278  addnq0mo  7464  mulnq0mo  7465  ltexprlemdisj  7623  recexprlemdisj  7647  addsrmo  7760  mulsrmo  7761  summodc  11409  prodmodc  11604  pceu  12313  rhmex  13468  limcimo  14531  exmidsbth  15170
  Copyright terms: Public domain W3C validator