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

Theorem alrimi 1431
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 1428 . 2 (𝜑 → ∀𝑥𝜑)
3 alrimi.2 . 2 (𝜑𝜓)
42, 3alrimih 1374 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257  wnf 1365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-5 1352  ax-gen 1354  ax-4 1416
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  19.32r  1586  cbv3  1646  sbalyz  1891  dvelimdf  1908  dvelimor  1910  abbid  2170  nfcd  2189  ralrimi  2407  r19.32r  2474  ceqsalg  2599  ceqsex  2609  vtocldf  2622  elrab3t  2720  morex  2748  sbciedf  2821  csbiebt  2914  csbiedf  2915  ssrd  2978  rgenm  3351  invdisj  3787  ssopab2b  4041  eusv2nf  4216  sniota  4922  imadif  5007  funimaexglem  5010  eusvobj1  5527  ssoprab2b  5590  ovmpt2dxf  5654
  Copyright terms: Public domain W3C validator