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 1445 1 (𝜑 → ∀𝑥𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1329  Ⅎwnf 1436 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1423  ax-gen 1425  ax-4 1487 This theorem depends on definitions:  df-bi 116  df-nf 1437 This theorem is referenced by:  19.32r  1658  cbv3  1720  sbbid  1818  sbalyz  1974  dvelimdf  1991  dvelimor  1993  abbid  2256  nfcd  2276  ralrimi  2503  r19.32r  2578  ceqsalg  2714  ceqsex  2724  vtocldf  2737  elrab3t  2839  morex  2868  sbciedf  2944  csbiebt  3039  csbiedf  3040  ssrd  3102  rgenm  3465  invdisj  3923  ssopab2b  4198  eusv2nf  4377  sniota  5115  imadif  5203  funimaexglem  5206  eusvobj1  5761  ssoprab2b  5828  ovmpodxf  5896
 Copyright terms: Public domain W3C validator