Theorem alrimiv 1924

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

Syntax hints:   → wi 4  ∀wal 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem is referenced by:  alrimivv  1925  cbvalivw  2003  aevlem0  2051  aev  2054  aev2  2055  stdpc4  2065  sbimdv  2075  sbbidv  2076  elequ2g  2121  cbv3v2  2238  nexmo  2538  moimdv  2543  mobidv  2546  eubidv  2583  euequ  2594  eqrdv  2732  abbidv  2805  raleqbidvvOLD  3332  elex2OLD  3502  elex22  3503  ceqsexvOLD  3530  pm13.183  3665  moeq3  3720  sbc2or  3799  sbcthdv  3806  sbcimdvOLD  3865  csbied  3945  ssrdv  4000  abssdvOLD  4078  eq0rdv  4412  disj  4455  rabeqsnd  4673  rabsn  4725  dfnfc2  4933  intab  4982  intprg  4985  iuneq12df  5022  dfiin2g  5036  mpteq12dvaOLD  5237  abexd  5330  elALT2  5374  reusv2lem1  5403  reusv2lem2  5404  axprlem3OLD  5433  sbcop1  5498  euotd  5522  ssrelrel  5808  asymref2  6139  dfpo2  6317  iotaval2  6530  iotavalOLD  6536  iota5  6545  iotabidv  6546  funmo  6582  funmoOLD  6583  funco  6607  funun  6613  fununfun  6615  fununi  6642  nfunsn  6948  fvn0ssdmfun  7093  f1oresrab  7146  0mpo0  7515  funoprabg  7553  tfisi  7879  limom  7902  funcnvuni  7954  1stconst  8123  2ndconst  8124  frxp  8149  fnwelem  8154  frxp2  8167  frxp3  8174  frrlem9  8317  seqomlem2  8489  iserd  8769  fsetdmprc0  8893  ssfi  9211  findcard3  9315  findcard3OLD  9316  frfi  9318  fiint  9363  fiintOLD  9364  dffi2  9460  hartogslem1  9579  wdomd  9618  ixpiunwdom  9627  ttrclss  9757  ttrclselem2  9763  rankval3b  9863  fseqenlem2  10062  dfac3  10158  dfac5  10166  dfac2b  10168  dfac8  10173  dfac9  10174  dfacacn  10179  dfac13  10180  kmlem1  10188  kmlem6  10193  kmlem13  10200  fin23lem32  10381  axdc2lem  10485  zornn0g  10542  fpwwe2lem10  10677  fpwwe2lem11  10678  fpwwe2lem12  10679  hargch  10710  alephgch  10711  nqpr  11051  reclem2pr  11085  hashgt23el  14459  cshwsexaOLD  14859  rtrclreclem4  15096  dfrtrcl2  15097  relexpindlem  15098  shftfn  15108  ramub  17046  ramcl  17062  imasaddfnlem  17574  imasvscafn  17583  mrieqv2d  17683  mreexexd  17692  invfun  17811  joinfval  18430  meetfval  18444  mreclatBAD  18620  letsr  18650  efgval  19749  efgi  19751  efgi2  19757  gsumval3lem2  19938  gsumzaddlem  19953  pgpfac1lem5  20113  ringurd  20202  zrinitorngc  20658  zrtermorngc  20659  zrtermoringc  20691  islbs3  21174  lbsextlem4  21180  cssmre  21728  obslbs  21767  mplsubglem  22036  mpllsslem  22037  tgcl  22991  indistopon  23023  ppttop  23029  epttop  23031  mretopd  23115  toponmre  23116  neissex  23150  neiptoptop  23154  lmfun  23404  2ndcdisj  23479  1stccnp  23485  kgentopon  23561  dfac14  23641  ptcnp  23645  uptx  23648  ptrescn  23662  qtoptop2  23722  filconn  23906  filssufilg  23934  rnelfmlem  23975  alexsubALTlem2  24071  cnextfun  24087  utoptop  24258  prdsxmslem2  24557  vitalilem3  25658  mbfposr  25700  mbfinf  25713  i1fd  25729  itg1climres  25763  perfdvf  25952  taylf  26416  addsbdaylem  28063  noseqrdgfn  28326  n0scut  28352  mptelee  28924  upgr1eopALT  29148  upgrspanop  29328  umgrspanop  29329  usgrspanop  29330  cplgrop  29468  umgr2v2enb1  29558  clwwlknon1loop  30126  wlkl0  30395  ex-natded9.26  30447  ex-natded9.26-2  30448  aevdemo  30488  nmcexi  32054  iuneq12daf  32576  iinabrex  32588  abfmpeld  32670  abfmpel  32671  fpwrelmap  32750  ssdifidl  33464  ssmxidl  33481  zarclssn  33833  bnj1143  34782  bnj1379  34822  bnj149  34867  fineqvac  35089  gblacfnacd  35091  wevgblacfn  35092  loop1cycl  35121  satffunlem1lem1  35386  satffunlem2lem1  35388  prv0  35414  mclsssvlem  35546  ssmclslem  35549  mclsax  35553  mclsind  35554  dfon2lem6  35769  dfon2lem8  35771  dfon2lem9  35772  dfon2  35773  trer  36298  finminlem  36300  neibastop1  36341  neibastop3  36344  weiunfr  36449  unbdqndv1  36490  knoppndv  36516  bj-ssbid1ALT  36647  bj-eqs  36657  bj-sb  36669  bj-substw  36704  bj-nnfbd  36708  bj-spcimdv  36877  bj-spcimdvv  36878  bj-csbprc  36892  bj-gabss  36917  bj-elgab  36921  curryset  36928  currysetlem3  36931  bj-cleq  36944  exellimddv  37327  finorwe  37364  wl-motae  37495  wl-cbvalsbi  37526  fin2so  37593  poimirlem17  37623  mblfinlem3  37645  ismblfin  37647  itg2addnc  37660  upixp  37715  mpobi123f  38148  mptbi12f  38152  trcoss  38463  prter1  38860  axc11n-16  38919  ax12eq  38922  ax12el  38923  sticksstones22  42149  sbtd  42228  sn-axprlem3  42234  sn-exelALT  42235  ismrcd1  42685  ttac  43024  fnwe2  43041  aomclem6  43047  dfac11  43050  dfac21  43054  hbtlem2  43112  oaun3lem1  43363  cllem0  43555  clss2lem  43600  mptrcllem  43602  iunrelexpmin1  43697  iunrelexpmin2  43701  iunrelexpuztr  43708  dftrcl3  43709  brtrclfv2  43716  dfrtrcl3  43722  psshepw  43777  frege91  43943  frege97  43949  frege109  43961  frege130  43982  grumnudlem  44280  ismnushort  44296  axc11next  44401  pm13.192  44405  pm14.24  44427  gen11  44613  trsspwALT2  44816  snssiALT  44825  sstrALT2  44832  en3lpVD  44842  sspwimp  44915  sspwimpcf  44917  sspwimpALT  44922  ax6e2ndeqALT  44928  ssmapsn  45158  infnsuprnmpt  45194  uzinico  45512  icccncfext  45842  itgsinexplem1  45909  sge0resplit  46361  hoidmvlelem1  46550  hspdifhsp  46571  smflimsuplem7  46781  dfatcolem  47204  iccpartdisj  47361  sbcpr  47445  eufsnlem  48670  iscnrm3lem2  48730  setrec2fun  48922  elsetrecslem  48929  setrecsss  48931  setrecsres  48932  0setrec  48934  pgindnf  48946