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

Theorem alrimi 1502
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 1499 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1449 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1333  wnf 1440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1427  ax-gen 1429  ax-4 1490
This theorem depends on definitions:  df-bi 116  df-nf 1441
This theorem is referenced by:  axc4i  1522  19.32r  1660  cbv3  1722  sbbid  1826  sbalyz  1979  dvelimdf  1996  dvelimor  1998  nf5d  2005  abbid  2274  nfcd  2294  nfabdw  2318  ralrimi  2528  r19.32r  2603  ceqsalg  2740  ceqsex  2750  vtocldf  2763  elrab3t  2867  morex  2896  sbciedf  2972  csbiebt  3070  csbiedf  3071  ssrd  3133  rgenm  3496  invdisj  3959  ssopab2b  4236  eusv2nf  4416  sniota  5162  imadif  5250  funimaexglem  5253  eusvobj1  5811  ssoprab2b  5878  ovmpodxf  5946
  Copyright terms: Public domain W3C validator