Theorem alrimiv 1929

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem is referenced by:  alrimivv  1930  cbvalivw  2009  aevlem0  2058  aev  2061  aev2  2062  stdpc4  2074  sbimdv  2084  sbbidv  2085  elequ2g  2130  cbv3v2  2249  nexmo  2542  moimdv  2547  mobidv  2550  eubidv  2587  euequ  2598  eqrdv  2735  abbidv  2803  elex22  3455  pm13.183  3609  moeq3  3659  sbc2or  3738  sbcthdv  3745  csbied  3874  ssrdv  3928  eq0rdv  4348  rabeqsnd  4614  rabsn  4666  dfnfc2  4873  intab  4921  iuneq12df  4961  elALT2  5308  reusv2lem1  5337  reusv2lem2  5338  axprlem3OLD  5368  sbcop1  5438  euotd  5463  ssrelrel  5747  relimasn  6046  asymref2  6076  dfpo2  6256  iotaval2  6465  iota5  6477  iotabidv  6478  funmo  6510  funco  6534  funun  6540  fununfun  6542  fununi  6569  nfunsn  6875  fvn0ssdmfun  7022  f1oresrab  7076  0mpo0  7445  funoprabg  7483  tfisi  7805  limom  7828  funcnvuni  7878  1stconst  8045  2ndconst  8046  frxp  8071  fnwelem  8076  frxp2  8089  frxp3  8096  frrlem9  8239  seqomlem2  8385  iserd  8665  fsetdmprc0  8797  ssfi  9102  findcard3  9188  frfi  9190  fiint  9232  dffi2  9331  hartogslem1  9452  wdomd  9491  ixpiunwdom  9500  ttrclss  9636  ttrclselem2  9642  rankval3b  9745  fseqenlem2  9942  dfac3  10038  dfac5  10046  dfac2b  10048  dfac8  10053  dfac9  10054  dfacacn  10059  dfac13  10060  kmlem1  10068  kmlem6  10073  kmlem13  10080  fin23lem32  10261  zornn0g  10422  fpwwe2lem10  10558  fpwwe2lem11  10559  fpwwe2lem12  10560  hargch  10591  alephgch  10592  nqpr  10932  reclem2pr  10966  hashgt23el  14381  rtrclreclem4  15018  dfrtrcl2  15019  relexpindlem  15020  shftfn  15030  ramub  16979  ramcl  16995  imasaddfnlem  17487  imasvscafn  17496  mrieqv2d  17600  mreexexd  17609  invfun  17726  joinfval  18332  meetfval  18346  mreclatBAD  18524  letsr  18554  efgval  19687  efgi  19689  efgi2  19695  gsumval3lem2  19876  gsumzaddlem  19891  pgpfac1lem5  20051  ringurd  20161  zrinitorngc  20614  zrtermorngc  20615  zrtermoringc  20647  islbs3  21149  lbsextlem4  21155  cssmre  21687  obslbs  21724  mplsubglem  21991  mpllsslem  21992  tgcl  22948  indistopon  22980  ppttop  22986  epttop  22988  mretopd  23071  toponmre  23072  neissex  23106  neiptoptop  23110  lmfun  23360  2ndcdisj  23435  1stccnp  23441  kgentopon  23517  dfac14  23597  ptcnp  23601  uptx  23604  ptrescn  23618  qtoptop2  23678  filconn  23862  filssufilg  23890  rnelfmlem  23931  alexsubALTlem2  24027  cnextfun  24043  utoptop  24213  prdsxmslem2  24508  vitalilem3  25591  mbfposr  25633  mbfinf  25646  i1fd  25662  itg1climres  25695  perfdvf  25884  taylf  26341  addbdaylem  28027  noseqrdgfn  28316  n0cut  28344  mpteleeOLD  28982  upgr1eopALT  29204  upgrspanop  29384  umgrspanop  29385  usgrspanop  29386  cplgrop  29524  umgr2v2enb1  29614  clwwlknon1loop  30187  wlkl0  30456  ex-natded9.26  30508  ex-natded9.26-2  30509  aevdemo  30549  nmcexi  32116  iuneq12daf  32645  iinabrex  32658  abfmpeld  32746  abfmpel  32747  ssdifidl  33536  ssmxidl  33553  exsslsb  33760  zarclssn  34037  bnj1143  34952  bnj1379  34992  bnj149  35037  rankval4b  35263  r1omhfb  35276  fineqvac  35280  r1omhfbregs  35301  gblacfnacd  35304  vonf1owev  35310  wevgblacfn  35311  loop1cycl  35339  satffunlem1lem1  35604  satffunlem2lem1  35606  prv0  35632  mclsssvlem  35764  ssmclslem  35767  mclsax  35771  mclsind  35772  dfon2lem6  35988  dfon2lem8  35990  dfon2lem9  35991  dfon2  35992  trer  36518  finminlem  36520  neibastop1  36561  neibastop3  36564  weiunfr  36669  axuntco  36681  regsfromunir1  36742  mh-regprimbi  36747  unbdqndv1  36788  knoppndv  36814  bj-ssbid1ALT  36979  bj-eqs  36990  bj-sb  37004  bj-substw  37042  bj-spcimdv  37222  bj-spcimdvv  37223  bj-csbprc  37237  bj-gabss  37262  bj-elgab  37266  curryset  37273  currysetlem3  37276  bj-cleq  37289  exellimddv  37679  finorwe  37716  wl-motae  37858  wl-cbvalsbi  37889  fin2so  37946  poimirlem17  37976  mblfinlem3  37998  ismblfin  38000  itg2addnc  38013  upixp  38068  mpobi123f  38501  mptbi12f  38505  preuniqval  38835  trcoss  38911  eldisjsim5  39278  prter1  39343  axc11n-16  39402  ax12eq  39405  ax12el  39406  sticksstones22  42625  sbtd  42668  sn-axprlem3  42677  sn-exelALT  42678  ismrcd1  43148  ttac  43486  fnwe2  43503  aomclem6  43509  dfac11  43512  dfac21  43516  hbtlem2  43574  oaun3lem1  43824  cllem0  44015  clss2lem  44060  mptrcllem  44062  iunrelexpmin1  44157  iunrelexpmin2  44161  iunrelexpuztr  44168  dftrcl3  44169  brtrclfv2  44176  dfrtrcl3  44182  psshepw  44237  frege91  44403  frege97  44409  frege109  44421  frege130  44442  grumnudlem  44734  ismnushort  44750  axc11next  44855  pm13.192  44859  pm14.24  44881  gen11  45065  trsspwALT2  45267  snssiALT  45276  sstrALT2  45283  en3lpVD  45293  sspwimp  45366  sspwimpcf  45368  sspwimpALT  45373  ax6e2ndeqALT  45379  ssmapsn  45667  infnsuprnmpt  45701  uzinico  46011  icccncfext  46337  itgsinexplem1  46404  sge0resplit  46856  hspdifhsp  47066  smflimsuplem7  47276  dfatcolem  47719  iccpartdisj  47913  sbcpr  47997  eufsnlem  49332  iscnrm3lem2  49426  functhincfun  49940  termcarweu  50019  setrec2fun  50183  elsetrecslem  50190  setrecsss  50192  setrecsres  50193  0setrec  50195  pgindnf  50207