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

Theorem alrimi 1415
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 1412 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1358 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1241  wnf 1349
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-5 1336  ax-gen 1338  ax-4 1400
This theorem depends on definitions:  df-bi 110  df-nf 1350
This theorem is referenced by:  19.32r  1570  cbv3  1630  sbalyz  1875  dvelimdf  1892  dvelimor  1894  abbid  2154  nfcd  2173  ralrimi  2390  r19.32r  2457  ceqsalg  2582  ceqsex  2592  vtocldf  2605  elrab3t  2697  morex  2725  sbciedf  2798  csbiebt  2886  csbiedf  2887  ssrd  2950  rgenm  3323  invdisj  3759  ssopab2b  4013  eusv2nf  4188  sniota  4894  imadif  4979  funimaexglem  4982  eusvobj1  5499  ssoprab2b  5562  ovmpt2dxf  5626
  Copyright terms: Public domain W3C validator