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

Theorem alrimi 1412
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
alrimi.1  F/
alrimi.2
Assertion
Ref Expression
alrimi

Proof of Theorem alrimi
StepHypRef Expression
1 alrimi.1 . . 3  F/
21nfri 1409 . 2
3 alrimi.2 . 2
42, 3alrimih 1355 1
Colors of variables: wff set class
Syntax hints:   wi 4  wal 1240   F/wnf 1346
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-5 1333  ax-gen 1335  ax-4 1397
This theorem depends on definitions:  df-bi 110  df-nf 1347
This theorem is referenced by:  19.32r  1567  cbv3  1627  sbalyz  1872  dvelimdf  1889  dvelimor  1891  abbid  2151  nfcd  2170  ralrimi  2384  r19.32r  2451  ceqsalg  2576  ceqsex  2586  vtocldf  2599  elrab3t  2691  morex  2719  sbciedf  2792  csbiebt  2880  csbiedf  2881  ssrd  2944  rgenm  3317  invdisj  3750  ssopab2b  4004  eusv2nf  4154  sniota  4837  imadif  4922  funimaexglem  4925  eusvobj1  5442  ssoprab2b  5504  ovmpt2dxf  5568
  Copyright terms: Public domain W3C validator