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

Theorem alrimivv 1855
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 1854 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1854 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1427  ax-gen 1429  ax-17 1506
This theorem is referenced by:  2ax17  1858  euind  2899  sbnfc2  3091  exmidsssn  4163  exmidel  4166  exmidundif  4167  exmidundifim  4168  ssopab2dv  4238  suctr  4381  eusvnf  4413  ordsuc  4522  ssrel  4674  relssdv  4678  eqrelrdv  4682  eqbrrdv  4683  eqrelrdv2  4685  ssrelrel  4686  iss  4912  funssres  5212  funun  5214  fununi  5238  fsn  5639  ovg  5959  caovimo  6014  oprabexd  6075  qliftfund  6563  eroveu  6571  th3qlem1  6582  exmidfodomrlemim  7136  addnq0mo  7367  mulnq0mo  7368  ltexprlemdisj  7526  recexprlemdisj  7550  addsrmo  7663  mulsrmo  7664  summodc  11280  prodmodc  11475  limcimo  13034  exmidsbth  13595
  Copyright terms: Public domain W3C validator