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

Theorem alrimivv 1868
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 1867 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1867 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1440  ax-gen 1442  ax-17 1519
This theorem is referenced by:  2ax17  1871  euind  2917  sbnfc2  3109  exmidsssn  4188  exmidel  4191  exmidundif  4192  exmidundifim  4193  ssopab2dv  4263  suctr  4406  eusvnf  4438  ordsuc  4547  ssrel  4699  relssdv  4703  eqrelrdv  4707  eqbrrdv  4708  eqrelrdv2  4710  ssrelrel  4711  iss  4937  funssres  5240  funun  5242  fununi  5266  fsn  5668  ovg  5991  caovimo  6046  oprabexd  6106  qliftfund  6596  eroveu  6604  th3qlem1  6615  exmidfodomrlemim  7178  addnq0mo  7409  mulnq0mo  7410  ltexprlemdisj  7568  recexprlemdisj  7592  addsrmo  7705  mulsrmo  7706  summodc  11346  prodmodc  11541  pceu  12249  limcimo  13428  exmidsbth  14056
  Copyright terms: Public domain W3C validator