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

Theorem alrimi 1522
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
alrimi.1 𝑥𝜑
alrimi.2 (𝜑𝜓)
Assertion
Ref Expression
alrimi (𝜑 → ∀𝑥𝜓)

Proof of Theorem alrimi
StepHypRef Expression
1 alrimi.1 . . 3 𝑥𝜑
21nfri 1519 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1469 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1351  wnf 1460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1447  ax-gen 1449  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-nf 1461
This theorem is referenced by:  axc4i  1542  19.32r  1680  cbv3  1742  sbbid  1846  sbalyz  1999  dvelimdf  2016  dvelimor  2018  nf5d  2025  abbid  2294  nfcd  2314  nfabdw  2338  ralrimi  2548  r19.32r  2623  ceqsalg  2765  ceqsex  2775  vtocldf  2788  elrab3t  2892  morex  2921  sbciedf  2998  csbiebt  3096  csbiedf  3097  ssrd  3160  rgenm  3525  invdisj  3997  ssopab2b  4276  eusv2nf  4456  sniota  5207  imadif  5296  funimaexglem  5299  eusvobj1  5861  ssoprab2b  5931  ovmpodxf  5999
  Copyright terms: Public domain W3C validator