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

Theorem alrimivv 1771
 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 1770 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1770 1 (𝜑 → ∀𝑥𝑦𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1257 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1352  ax-gen 1354  ax-17 1435 This theorem is referenced by:  2ax17  1774  euind  2751  sbnfc2  2934  ssopab2dv  4043  suctr  4186  eusvnf  4213  ordsuc  4315  ssrel  4456  relssdv  4460  eqrelrdv  4464  eqbrrdv  4465  eqrelrdv2  4467  ssrelrel  4468  iss  4682  funssres  4970  funun  4972  fununi  4995  fsn  5363  ovg  5667  caovimo  5722  oprabexd  5782  qliftfund  6220  eroveu  6228  th3qlem1  6239  addnq0mo  6603  mulnq0mo  6604  ltexprlemdisj  6762  recexprlemdisj  6786  addsrmo  6886  mulsrmo  6887
 Copyright terms: Public domain W3C validator