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

Theorem alrimivv 1804
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 1803 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1803 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1288
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1382  ax-gen 1384  ax-17 1465
This theorem is referenced by:  2ax17  1807  euind  2803  sbnfc2  2989  exmidsssn  4040  exmidel  4042  exmidundif  4043  exmidundifim  4044  ssopab2dv  4114  suctr  4257  eusvnf  4288  ordsuc  4392  ssrel  4539  relssdv  4543  eqrelrdv  4547  eqbrrdv  4548  eqrelrdv2  4550  ssrelrel  4551  iss  4771  funssres  5069  funun  5071  fununi  5095  fsn  5483  ovg  5797  caovimo  5852  oprabexd  5912  qliftfund  6389  eroveu  6397  th3qlem1  6408  exmidfodomrlemim  6888  addnq0mo  7067  mulnq0mo  7068  ltexprlemdisj  7226  recexprlemdisj  7250  addsrmo  7350  mulsrmo  7351  isummo  10834  exmidsbth  12186
  Copyright terms: Public domain W3C validator