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  2541  moimdv  2546  mobidv  2549  eubidv  2586  euequ  2597  eqrdv  2734  abbidv  2802  elex22  3454  pm13.183  3608  moeq3  3658  sbc2or  3737  sbcthdv  3744  csbied  3873  ssrdv  3927  eq0rdv  4347  rabeqsnd  4613  rabsn  4665  dfnfc2  4872  intab  4920  iuneq12df  4960  elALT2  5311  reusv2lem1  5340  reusv2lem2  5341  axprlem3OLD  5371  sbcop1  5441  euotd  5467  ssrelrel  5752  relimasn  6050  asymref2  6080  dfpo2  6260  iotaval2  6469  iota5  6481  iotabidv  6482  funmo  6514  funco  6538  funun  6544  fununfun  6546  fununi  6573  nfunsn  6879  fvn0ssdmfun  7026  f1oresrab  7080  0mpo0  7450  funoprabg  7488  tfisi  7810  limom  7833  funcnvuni  7883  1stconst  8050  2ndconst  8051  frxp  8076  fnwelem  8081  frxp2  8094  frxp3  8101  frrlem9  8244  seqomlem2  8390  iserd  8670  fsetdmprc0  8802  ssfi  9107  findcard3  9193  frfi  9195  fiint  9237  dffi2  9336  hartogslem1  9457  wdomd  9496  ixpiunwdom  9505  ttrclss  9641  ttrclselem2  9647  rankval3b  9750  fseqenlem2  9947  dfac3  10043  dfac5  10051  dfac2b  10053  dfac8  10058  dfac9  10059  dfacacn  10064  dfac13  10065  kmlem1  10073  kmlem6  10078  kmlem13  10085  fin23lem32  10266  zornn0g  10427  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2lem12  10565  hargch  10596  alephgch  10597  nqpr  10937  reclem2pr  10971  hashgt23el  14386  rtrclreclem4  15023  dfrtrcl2  15024  relexpindlem  15025  shftfn  15035  ramub  16984  ramcl  17000  imasaddfnlem  17492  imasvscafn  17501  mrieqv2d  17605  mreexexd  17614  invfun  17731  joinfval  18337  meetfval  18351  mreclatBAD  18529  letsr  18559  efgval  19692  efgi  19694  efgi2  19700  gsumval3lem2  19881  gsumzaddlem  19896  pgpfac1lem5  20056  ringurd  20166  zrinitorngc  20619  zrtermorngc  20620  zrtermoringc  20652  islbs3  21153  lbsextlem4  21159  cssmre  21673  obslbs  21710  mplsubglem  21977  mpllsslem  21978  tgcl  22934  indistopon  22966  ppttop  22972  epttop  22974  mretopd  23057  toponmre  23058  neissex  23092  neiptoptop  23096  lmfun  23346  2ndcdisj  23421  1stccnp  23427  kgentopon  23503  dfac14  23583  ptcnp  23587  uptx  23590  ptrescn  23604  qtoptop2  23664  filconn  23848  filssufilg  23876  rnelfmlem  23917  alexsubALTlem2  24013  cnextfun  24029  utoptop  24199  prdsxmslem2  24494  vitalilem3  25577  mbfposr  25619  mbfinf  25632  i1fd  25648  itg1climres  25681  perfdvf  25870  taylf  26326  addbdaylem  28009  noseqrdgfn  28298  n0cut  28326  mpteleeOLD  28964  upgr1eopALT  29186  upgrspanop  29366  umgrspanop  29367  usgrspanop  29368  cplgrop  29506  umgr2v2enb1  29595  clwwlknon1loop  30168  wlkl0  30437  ex-natded9.26  30489  ex-natded9.26-2  30490  aevdemo  30530  nmcexi  32097  iuneq12daf  32626  iinabrex  32639  abfmpeld  32727  abfmpel  32728  ssdifidl  33517  ssmxidl  33534  exsslsb  33741  zarclssn  34017  bnj1143  34932  bnj1379  34972  bnj149  35017  rankval4b  35243  r1omhfb  35256  fineqvac  35260  r1omhfbregs  35281  gblacfnacd  35284  vonf1owev  35290  wevgblacfn  35291  loop1cycl  35319  satffunlem1lem1  35584  satffunlem2lem1  35586  prv0  35612  mclsssvlem  35744  ssmclslem  35747  mclsax  35751  mclsind  35752  dfon2lem6  35968  dfon2lem8  35970  dfon2lem9  35971  dfon2  35972  trer  36498  finminlem  36500  neibastop1  36541  neibastop3  36544  weiunfr  36649  axuntco  36661  regsfromunir1  36722  mh-regprimbi  36727  unbdqndv1  36768  knoppndv  36794  bj-ssbid1ALT  36959  bj-eqs  36970  bj-sb  36984  bj-substw  37022  bj-spcimdv  37202  bj-spcimdvv  37203  bj-csbprc  37217  bj-gabss  37242  bj-elgab  37246  curryset  37253  currysetlem3  37256  bj-cleq  37269  exellimddv  37661  finorwe  37698  wl-motae  37840  wl-cbvalsbi  37871  fin2so  37928  poimirlem17  37958  mblfinlem3  37980  ismblfin  37982  itg2addnc  37995  upixp  38050  mpobi123f  38483  mptbi12f  38487  preuniqval  38817  trcoss  38893  eldisjsim5  39260  prter1  39325  axc11n-16  39384  ax12eq  39387  ax12el  39388  sticksstones22  42607  sbtd  42650  sn-axprlem3  42659  sn-exelALT  42660  ismrcd1  43130  ttac  43464  fnwe2  43481  aomclem6  43487  dfac11  43490  dfac21  43494  hbtlem2  43552  oaun3lem1  43802  cllem0  43993  clss2lem  44038  mptrcllem  44040  iunrelexpmin1  44135  iunrelexpmin2  44139  iunrelexpuztr  44146  dftrcl3  44147  brtrclfv2  44154  dfrtrcl3  44160  psshepw  44215  frege91  44381  frege97  44387  frege109  44399  frege130  44420  grumnudlem  44712  ismnushort  44728  axc11next  44833  pm13.192  44837  pm14.24  44859  gen11  45043  trsspwALT2  45245  snssiALT  45254  sstrALT2  45261  en3lpVD  45271  sspwimp  45344  sspwimpcf  45346  sspwimpALT  45351  ax6e2ndeqALT  45357  ssmapsn  45645  infnsuprnmpt  45679  uzinico  45989  icccncfext  46315  itgsinexplem1  46382  sge0resplit  46834  hspdifhsp  47044  smflimsuplem7  47254  dfatcolem  47703  iccpartdisj  47897  sbcpr  47981  eufsnlem  49316  iscnrm3lem2  49410  functhincfun  49924  termcarweu  50003  setrec2fun  50167  elsetrecslem  50174  setrecsss  50176  setrecsres  50177  0setrec  50179  pgindnf  50191