Theorem alrimiv 1928

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2198 and 19.21v 1940. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
alrimiv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alrimiv	⊢ (𝜑 → ∀𝑥𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem alrimiv

Step	Hyp	Ref	Expression
1		ax-5 1911	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alrimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	alrimih 1824	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1911

This theorem is referenced by:  alrimivv  1929  cbvalivw  2008  aevlem0  2055  aev  2058  aev2  2059  stdpc4  2069  sbimdv  2079  sbbidv  2080  elequ2g  2120  cbv3v2  2232  nexmo  2533  moimdv  2538  mobidv  2541  eubidv  2578  euequ  2589  eqrdv  2728  abbidv  2799  raleqbidvvOLD  3328  elex2OLD  3494  elex22  3495  ceqsexvOLD  3525  pm13.183  3655  moeq3  3707  sbc2or  3785  sbcthdv  3792  sbcimdvOLD  3851  csbied  3930  ssrdv  3987  ss2abdvOLD  4061  abssdvOLD  4065  eq0rdv  4403  disj  4446  rabeqsnd  4670  rabsn  4724  dfnfc2  4932  intab  4981  intprg  4984  iuneq12df  5022  dfiin2g  5034  mpteq12dvaOLD  5237  elALT2  5366  reusv2lem1  5395  reusv2lem2  5396  axprlem3  5422  sbcop1  5487  euotd  5512  ssrelrel  5795  asymref2  6117  dfpo2  6294  iotaval2  6510  iotavalOLD  6516  iota5  6525  iotabidv  6526  funmo  6562  funmoOLD  6563  funco  6587  funun  6593  fununfun  6595  fununi  6622  nfunsn  6932  fvn0ssdmfun  7075  f1oresrab  7126  0mpo0  7494  funoprabg  7531  tfisi  7850  limom  7873  funcnvuni  7924  1stconst  8088  2ndconst  8089  frxp  8114  fnwelem  8119  frxp2  8132  frxp3  8139  frrlem9  8281  seqomlem2  8453  iserd  8731  fsetdmprc0  8851  ssfi  9175  findcard3  9287  findcard3OLD  9288  frfi  9290  fiint  9326  dffi2  9420  hartogslem1  9539  wdomd  9578  ixpiunwdom  9587  ttrclss  9717  ttrclselem2  9723  rankval3b  9823  fseqenlem2  10022  dfac3  10118  dfac5  10125  dfac2b  10127  dfac8  10132  dfac9  10133  dfacacn  10138  dfac13  10139  kmlem1  10147  kmlem6  10152  kmlem13  10159  fin23lem32  10341  axdc2lem  10445  zornn0g  10502  fpwwe2lem10  10637  fpwwe2lem11  10638  fpwwe2lem12  10639  hargch  10670  alephgch  10671  nqpr  11011  reclem2pr  11045  hashgt23el  14388  cshwsexaOLD  14779  rtrclreclem4  15012  dfrtrcl2  15013  relexpindlem  15014  shftfn  15024  ramub  16950  ramcl  16966  imasaddfnlem  17478  imasvscafn  17487  mrieqv2d  17587  mreexexd  17596  invfun  17715  joinfval  18330  meetfval  18344  mreclatBAD  18520  letsr  18550  efgval  19626  efgi  19628  efgi2  19634  gsumval3lem2  19815  gsumzaddlem  19830  pgpfac1lem5  19990  ringurd  20079  islbs3  20913  lbsextlem4  20919  cssmre  21465  obslbs  21504  mplsubglem  21777  mpllsslem  21778  tgcl  22692  indistopon  22724  ppttop  22730  epttop  22732  mretopd  22816  toponmre  22817  neissex  22851  neiptoptop  22855  lmfun  23105  2ndcdisj  23180  1stccnp  23186  kgentopon  23262  dfac14  23342  ptcnp  23346  uptx  23349  ptrescn  23363  qtoptop2  23423  filconn  23607  filssufilg  23635  rnelfmlem  23676  alexsubALTlem2  23772  cnextfun  23788  utoptop  23959  prdsxmslem2  24258  vitalilem3  25359  mbfposr  25401  mbfinf  25414  i1fd  25430  itg1climres  25464  perfdvf  25652  taylf  26109  n0scut  27943  mptelee  28420  upgr1eopALT  28644  upgrspanop  28821  umgrspanop  28822  usgrspanop  28823  cplgrop  28961  umgr2v2enb1  29050  clwwlknon1loop  29618  wlkl0  29887  ex-natded9.26  29939  ex-natded9.26-2  29940  aevdemo  29980  nmcexi  31546  iuneq12daf  32055  iinabrex  32067  abfmpeld  32146  abfmpel  32147  fpwrelmap  32225  ssmxidl  32864  zarclssn  33151  bnj1143  34099  bnj1379  34139  bnj149  34184  fineqvac  34395  loop1cycl  34426  satffunlem1lem1  34691  satffunlem2lem1  34693  prv0  34719  mclsssvlem  34851  ssmclslem  34854  mclsax  34858  mclsind  34859  dfon2lem6  35064  dfon2lem8  35066  dfon2lem9  35067  dfon2  35068  trer  35504  finminlem  35506  neibastop1  35547  neibastop3  35550  unbdqndv1  35687  knoppndv  35713  bj-ssbid1ALT  35845  bj-eqs  35855  bj-sb  35868  bj-substw  35903  bj-nnfbd  35907  bj-spcimdv  36078  bj-spcimdvv  36079  bj-csbprc  36093  bj-gabss  36118  bj-elgab  36122  curryset  36130  currysetlem3  36133  bj-cleq  36146  exellimddv  36529  finorwe  36566  wl-motae  36687  wl-cbvalsbi  36717  fin2so  36778  poimirlem17  36808  mblfinlem3  36830  ismblfin  36832  itg2addnc  36845  upixp  36900  mpobi123f  37333  mptbi12f  37337  trcoss  37655  prter1  38052  axc11n-16  38111  ax12eq  38114  ax12el  38115  sticksstones22  41290  sbtd  41333  sn-axprlem3  41340  sn-exelALT  41341  ismrcd1  41738  ttac  42077  fnwe2  42097  aomclem6  42103  dfac11  42106  dfac21  42110  hbtlem2  42168  oaun3lem1  42426  cllem0  42619  clss2lem  42664  mptrcllem  42666  iunrelexpmin1  42761  iunrelexpmin2  42765  iunrelexpuztr  42772  dftrcl3  42773  brtrclfv2  42780  dfrtrcl3  42786  psshepw  42841  frege91  43007  frege97  43013  frege109  43025  frege130  43046  grumnudlem  43346  ismnushort  43362  axc11next  43467  pm13.192  43471  pm14.24  43493  gen11  43679  trsspwALT2  43882  snssiALT  43891  sstrALT2  43898  en3lpVD  43908  sspwimp  43981  sspwimpcf  43983  sspwimpALT  43988  ax6e2ndeqALT  43994  ssmapsn  44213  infnsuprnmpt  44252  uzinico  44571  icccncfext  44901  itgsinexplem1  44968  sge0resplit  45420  hoidmvlelem1  45609  hspdifhsp  45630  smflimsuplem7  45840  dfatcolem  46261  iccpartdisj  46403  sbcpr  46487  zrinitorngc  46986  zrtermorngc  46987  zrtermoringc  47056  eufsnlem  47594  iscnrm3lem2  47654  setrec2fun  47824  elsetrecslem  47831  setrecsss  47833  setrecsres  47834  0setrec  47836  pgindnf  47848