Theorem alrimiv 1961

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2246 and 19.21v 1973. (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 1944	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alrimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	alrimih 1856	1 ⊢ (𝜑 → ∀𝑥𝜓)

This proof depends on syntax axioms:   → wi 4  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1827  ax-4 1841  ax-5 1944

This theorem is used by:  alrimivv  1962  cbvalivw  2041  aevlem0  2090  aev  2093  aev2  2094  stdpc4  2106  sbimdv  2116  sbbidv  2117  elequ2g  2162  cbv3v2  2280  nexmo  2569  moimdv  2574  mobidv  2577  eubidv  2614  euequ  2625  eqrdv  2761  abbidv  2829  elex22  3478  pm13.183  3623  moeq3  3673  sbc2or  3751  sbcthdv  3758  csbied  3887  ssrdv  3919  eq0rdv  4368  rabeqsnd  4630  rabsn  4682  dfnfc2  4892  intab  4941  iuneq12df  4981  elALT2  5335  reusv2lem1  5364  reusv2lem2  5365  sbcop1  5462  euotd  5490  ssrelrel  5777  relimasn  6089  asymref2  6117  dfpo2  6306  iotaval2  6516  iota5  6529  iotabidv  6530  funmo  6563  funco  6589  funun  6595  fununfunOLD  6598  fununi  6626  nfunsn  6935  fvn0ssdmfun  7085  f1oresrab  7139  0mpo0  7513  funoprabg  7551  tfisi  7880  limom  7903  funcnvuni  7954  1stconst  8124  2ndconst  8125  frxp  8151  fnwelem  8156  fnwe2  8162  frxp2  8174  frxp3  8181  frrlem9  8326  seqomlem2  8475  iserd  8758  fsetdmprc0  8891  ssfi  9202  findcard3  9288  frfi  9290  fiint  9332  dffi2  9428  hartogslem1  9549  wdomd  9588  ixpiunwdom  9597  ttrclss  9734  ttrclselem2  9740  rankval3b  9849  rankval4b  9893  hfpw  9939  setrec2fun  9986  fseqenlem2  10117  dfac3  10213  dfac5  10220  dfac2b  10222  dfac8  10227  dfac9  10228  dfacacn  10233  dfac13  10234  kmlem1  10242  kmlem6  10247  kmlem13  10254  fin23lem32  10435  zornn0g  10596  fpwwe2lem10  10738  fpwwe2lem11  10739  fpwwe2lem12  10740  hargch  10771  alephgch  10772  nqpr  11112  reclem2pr  11146  hashgt23el  14582  rtrclreclem4  15229  dfrtrcl2  15230  relexpindlem  15231  shftfn  15241  ramub  17206  ramcl  17222  imasaddfnlem  17715  imasvscafn  17724  mrieqv2d  17828  mreexexd  17837  invfun  17954  joinfval  18560  meetfval  18574  mreclatBAD  18752  letsr  18782  efgval  19946  efgi  19948  efgi2  19954  gsumval3lem2  20135  gsumzaddlem  20150  pgpfac1lem5  20310  ringurd  20426  zrinitorngc  20909  zrtermorngc  20910  zrtermoringc  20942  islbs3  21448  lbsextlem4  21454  rspsn0  21541  ssdifidl  21656  cssmre  22014  obslbs  22051  mplsubglem  22321  mpllsslem  22322  tgcl  23302  indistopon  23334  ppttop  23340  epttop  23342  mretopd  23425  toponmre  23426  neissex  23460  neiptoptop  23464  lmfun  23714  2ndcdisj  23790  1stccnp  23796  kgentopon  23872  dfac14  23952  ptcnp  23956  uptx  23959  ptrescn  23973  qtoptop2  24033  filconn  24217  filssufilg  24245  rnelfmlem  24286  alexsubALTlem2  24382  cnextfun  24398  utoptop  24568  prdsxmslem2  24863  vitalilem3  25946  mbfposr  25988  mbfinf  26001  i1fd  26017  itg1climres  26050  perfdvf  26238  taylf  26703  addbdaylem  28418  noseqrdgfn  28707  n0cut  28735  mpteleeOLD  29488  upgr1eopALT  29710  upgrspanop  29893  umgrspanop  29894  usgrspanop  29895  cplgrop  30033  umgr2v2enb1  30122  clwwlknon1loop  30704  loop1cycl  30759  wlkl0  30983  ex-natded9.26  31035  ex-natded9.26-2  31036  aevdemo  31076  nmcexi  32643  iuneq12daf  33208  iinabrex  33220  abfmpeld  33305  abfmpel  33306  ssmxidl  34055  exsslsb  34285  zarclssn  34561  bnj1143  35476  bnj1379  35516  bnj149  35561  r1omhfb  35802  fineqvac  35858  r1omhfbregs  35879  kardval  35894  gblacfnacd  35986  vonf1wev  35993  vonf1owevOLD  35995  wevgblacfn  35996  vonf1onprcf1ac  36001  onprcf1acwevdlem2  36003  onprcf1of1orbd  36011  satffunlem1lem1  36291  satffunlem2lem1  36293  prv0  36319  mclsssvlem  36451  ssmclslem  36454  mclsax  36458  mclsind  36459  elpssmo  36591  dfon2lem6  36683  dfon2lem8  36685  dfon2lem9  36686  dfon2  36687  trer  37237  finminlem  37239  neibastop1  37280  neibastop3  37283  weiunfr  37388  axuntco  37400  regsfromunir1  37461  mh-regprimbi  37466  unbdqndv1  37507  knoppndv  37533  bj-ssbid1ALT  37697  bj-eqs  37708  bj-sb  37722  bj-substw  37760  bj-spcimdv  37940  bj-spcimdvv  37941  bj-csbprc  37955  bj-gabss  37981  bj-elgab  37985  curryset  37992  currysetlem3  37995  bj-cleq  38008  exellimddv  38414  finorwe  38451  wl-motae  38593  wl-cbvalsbi  38624  fin2so  38676  poimirlem17  38701  mblfinlem3  38723  ismblfin  38725  itg2addnc  38738  findcard4  38778  varprop  38788  negprop  38789  impprop  38790  upixp  38809  mpobi123f  39240  mptbi12f  39244  preuniqval  39574  trcoss  39650  eldisjsim5  40017  prter1  40082  axc11n-16  40141  ax12eq  40144  ax12el  40145  sticksstones22  43364  sbtd  43409  sn-axprlem3  43418  sn-exelALT  43419  ismrcd1  43855  ttac  44189  aomclem6  44207  dfac11  44210  dfac21  44214  hbtlem2  44272  oaun3lem1  44522  cllem0  44713  clss2lem  44757  mptrcllem  44759  iunrelexpmin1  44854  iunrelexpmin2  44858  iunrelexpuztr  44865  dftrcl3  44866  brtrclfv2  44873  dfrtrcl3  44879  psshepw  44934  frege91  45100  frege97  45106  frege109  45118  frege130  45139  grumnudlem  45415  ismnushort  45431  axc11next  45536  pm13.192  45540  pm14.24  45561  gen11  45744  trsspwALT2  45946  snssiALT  45955  sstrALT2  45962  en3lpVD  45972  sspwimp  46045  sspwimpcf  46047  sspwimpALT  46052  ax6e2ndeqALT  46058  ssmapsn  46374  infnsuprnmpt  46407  uzinico  46716  icccncfext  47042  itgsinexplem1  47109  sge0resplit  47561  hspdifhsp  47771  smflimsuplem7  47981  dfatcolem  48470  iccpartdisj  48664  sbcpr  48748  eufsnlem  50097  iscnrm3lem2  50194  functhincfun  50729  termcarweu  50808  elsetrecslem  51012  setrecsss  51014  setrecsres  51015  0setrec  51017  pgindnf  51029