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

Theorem alrimivv 1800
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 1799 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1799 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1379  ax-gen 1381  ax-17 1462
This theorem is referenced by:  2ax17  1803  euind  2793  sbnfc2  2977  exmidel  4008  exmidundif  4009  ssopab2dv  4079  suctr  4222  eusvnf  4249  ordsuc  4352  ssrel  4494  relssdv  4498  eqrelrdv  4502  eqbrrdv  4503  eqrelrdv2  4505  ssrelrel  4506  iss  4725  funssres  5021  funun  5023  fununi  5047  fsn  5432  ovg  5740  caovimo  5795  oprabexd  5855  qliftfund  6327  eroveu  6335  th3qlem1  6346  exmidfodomrlemim  6771  addnq0mo  6950  mulnq0mo  6951  ltexprlemdisj  7109  recexprlemdisj  7133  addsrmo  7233  mulsrmo  7234  isummo  10662  exmidsbth  11352
  Copyright terms: Public domain W3C validator