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