Theorem alrimi 1877

Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 1905. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
alrimi.1
alrimi.2

Assertion

Ref	Expression
alrimi

Proof of Theorem alrimi

Step	Hyp	Ref	Expression
1		alrimi.1	. . 3
2	1	nfri 1874	. 2
3		alrimi.2	. 2
4	2, 3	alrimih 1642	1

Syntax hints:  ->wi 4  A.wal 1393  F/wnf 1616

This theorem is referenced by:  nfd  1878  axc4i  1898  19.12  1950  nfald  1951  cbv3  2015  cbv2  2020  sbbid  2144  nfsbd  2186  mo3  2323  eupicka  2359  2moex  2365  2mo  2373  2moOLD  2374  axbnd  2434  abbid  2592  nfcd  2613  ralrimiOLD  2858  ceqsalgALT  3135  ceqsex  3145  vtocldf  3158  elrab3t  3256  morex  3283  sbciedf  3363  csbiebt  3454  csbiedf  3455  ssrd  3508  invdisj  4441  zfrepclf  4569  eusv2nf  4650  ssopab2b  4779  imadif  5668  eusvobj1  6290  ssoprab2b  6354  ovmpt2dxf  6428  axrepnd  8990  axunnd  8992  axpownd  8999  axregndlem1  9000  axacndlem1  9006  axacndlem2  9007  axacndlem3  9008  axacndlem4  9009  axacndlem5  9010  axacnd  9011  mreexexd  15045  acsmapd  15808  isch3  26159  ssrelf  27466  eqrelrd2  27467  esumeq12dvaf  28044  iota5f  29102  wl-mo3t  30021  wl-ax11-lem3  30027  cover2  30204  alrimii  30524  mpt2bi123f  30571  mptbi12f  30575  pm11.57  31295  pm11.59  31297  dvnmul  31740  stoweidlem34  31816  ovmpt2rdxf  32928  tratrb  33307  hbexg  33329  e2ebindALT  33729  bnj1366  33888  bnj571  33964  bnj964  34001  bj-hbext  34264  bj-nfext  34266  bj-cbv3v  34288  bj-cbv3v2  34289  bj-abbid  34364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617