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

Theorem alrimivv 1829
 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 1828 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1828 1 (𝜑 → ∀𝑥𝑦𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1312 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1406  ax-gen 1408  ax-17 1489 This theorem is referenced by:  2ax17  1832  euind  2842  sbnfc2  3028  exmidsssn  4093  exmidel  4096  exmidundif  4097  exmidundifim  4098  ssopab2dv  4168  suctr  4311  eusvnf  4342  ordsuc  4446  ssrel  4595  relssdv  4599  eqrelrdv  4603  eqbrrdv  4604  eqrelrdv2  4606  ssrelrel  4607  iss  4833  funssres  5133  funun  5135  fununi  5159  fsn  5558  ovg  5875  caovimo  5930  oprabexd  5991  qliftfund  6478  eroveu  6486  th3qlem1  6497  exmidfodomrlemim  7021  addnq0mo  7219  mulnq0mo  7220  ltexprlemdisj  7378  recexprlemdisj  7402  addsrmo  7515  mulsrmo  7516  summodc  11103  limcimo  12709  exmidsbth  13053
 Copyright terms: Public domain W3C validator