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  raleqbidvvOLD  3307  elex22  3467  pm13.183  3622  moeq3  3672  sbc2or  3751  sbcthdv  3758  csbied  3887  ssrdv  3941  eq0rdv  4361  rabeqsnd  4628  rabsn  4680  dfnfc2  4887  intab  4935  intprg  4938  iuneq12df  4975  dfiin2g  4988  elALT2  5318  reusv2lem1  5347  reusv2lem2  5348  axprlem3OLD  5377  sbcop1  5446  euotd  5471  ssrelrel  5755  relimasn  6054  asymref2  6084  dfpo2  6264  iotaval2  6473  iota5  6485  iotabidv  6486  funmo  6518  funco  6542  funun  6548  fununfun  6550  fununi  6577  nfunsn  6883  fvn0ssdmfun  7030  f1oresrab  7084  0mpo0  7453  funoprabg  7491  tfisi  7813  limom  7836  funcnvuni  7886  1stconst  8054  2ndconst  8055  frxp  8080  fnwelem  8085  frxp2  8098  frxp3  8105  frrlem9  8248  seqomlem2  8394  iserd  8674  fsetdmprc0  8806  ssfi  9111  findcard3  9197  frfi  9199  fiint  9241  dffi2  9340  hartogslem1  9461  wdomd  9500  ixpiunwdom  9509  ttrclss  9643  ttrclselem2  9649  rankval3b  9752  fseqenlem2  9949  dfac3  10045  dfac5  10053  dfac2b  10055  dfac8  10060  dfac9  10061  dfacacn  10066  dfac13  10067  kmlem1  10075  kmlem6  10080  kmlem13  10087  fin23lem32  10268  zornn0g  10429  fpwwe2lem10  10565  fpwwe2lem11  10566  fpwwe2lem12  10567  hargch  10598  alephgch  10599  nqpr  10939  reclem2pr  10973  hashgt23el  14361  rtrclreclem4  14998  dfrtrcl2  14999  relexpindlem  15000  shftfn  15010  ramub  16955  ramcl  16971  imasaddfnlem  17463  imasvscafn  17472  mrieqv2d  17576  mreexexd  17585  invfun  17702  joinfval  18308  meetfval  18322  mreclatBAD  18500  letsr  18530  efgval  19663  efgi  19665  efgi2  19671  gsumval3lem2  19852  gsumzaddlem  19867  pgpfac1lem5  20027  ringurd  20137  zrinitorngc  20592  zrtermorngc  20593  zrtermoringc  20625  islbs3  21127  lbsextlem4  21133  cssmre  21665  obslbs  21702  mplsubglem  21971  mpllsslem  21972  tgcl  22930  indistopon  22962  ppttop  22968  epttop  22970  mretopd  23053  toponmre  23054  neissex  23088  neiptoptop  23092  lmfun  23342  2ndcdisj  23417  1stccnp  23423  kgentopon  23499  dfac14  23579  ptcnp  23583  uptx  23586  ptrescn  23600  qtoptop2  23660  filconn  23844  filssufilg  23872  rnelfmlem  23913  alexsubALTlem2  24009  cnextfun  24025  utoptop  24195  prdsxmslem2  24490  vitalilem3  25584  mbfposr  25626  mbfinf  25639  i1fd  25655  itg1climres  25688  perfdvf  25877  taylf  26341  addbdaylem  28030  noseqrdgfn  28319  n0cut  28347  mpteleeOLD  28986  upgr1eopALT  29208  upgrspanop  29388  umgrspanop  29389  usgrspanop  29390  cplgrop  29528  umgr2v2enb1  29618  clwwlknon1loop  30191  wlkl0  30460  ex-natded9.26  30512  ex-natded9.26-2  30513  aevdemo  30553  nmcexi  32120  iuneq12daf  32649  iinabrex  32662  abfmpeld  32750  abfmpel  32751  ssdifidl  33556  ssmxidl  33573  exsslsb  33780  zarclssn  34057  bnj1143  34972  bnj1379  35012  bnj149  35057  rankval4b  35283  r1omhfb  35296  fineqvac  35300  r1omhfbregs  35321  gblacfnacd  35324  vonf1owev  35330  wevgblacfn  35331  loop1cycl  35359  satffunlem1lem1  35624  satffunlem2lem1  35626  prv0  35652  mclsssvlem  35784  ssmclslem  35787  mclsax  35791  mclsind  35792  dfon2lem6  36008  dfon2lem8  36010  dfon2lem9  36011  dfon2  36012  trer  36538  finminlem  36540  neibastop1  36581  neibastop3  36584  weiunfr  36689  exeltr  36693  regsfromunir1  36698  unbdqndv1  36736  knoppndv  36762  bj-ssbid1ALT  36927  bj-eqs  36938  bj-sb  36952  bj-substw  36990  bj-spcimdv  37170  bj-spcimdvv  37171  bj-csbprc  37185  bj-gabss  37210  bj-elgab  37214  curryset  37221  currysetlem3  37224  bj-cleq  37237  exellimddv  37627  finorwe  37664  wl-motae  37799  wl-cbvalsbi  37830  fin2so  37887  poimirlem17  37917  mblfinlem3  37939  ismblfin  37941  itg2addnc  37954  upixp  38009  mpobi123f  38442  mptbi12f  38446  preuniqval  38776  trcoss  38852  eldisjsim5  39219  prter1  39284  axc11n-16  39343  ax12eq  39346  ax12el  39347  sticksstones22  42567  sbtd  42610  sn-axprlem3  42619  sn-exelALT  42620  ismrcd1  43084  ttac  43422  fnwe2  43439  aomclem6  43445  dfac11  43448  dfac21  43452  hbtlem2  43510  oaun3lem1  43760  cllem0  43951  clss2lem  43996  mptrcllem  43998  iunrelexpmin1  44093  iunrelexpmin2  44097  iunrelexpuztr  44104  dftrcl3  44105  brtrclfv2  44112  dfrtrcl3  44118  psshepw  44173  frege91  44339  frege97  44345  frege109  44357  frege130  44378  grumnudlem  44670  ismnushort  44686  axc11next  44791  pm13.192  44795  pm14.24  44817  gen11  45001  trsspwALT2  45203  snssiALT  45212  sstrALT2  45219  en3lpVD  45229  sspwimp  45302  sspwimpcf  45304  sspwimpALT  45309  ax6e2ndeqALT  45315  ssmapsn  45603  infnsuprnmpt  45637  uzinico  45948  icccncfext  46274  itgsinexplem1  46341  sge0resplit  46793  hspdifhsp  47003  smflimsuplem7  47213  dfatcolem  47644  iccpartdisj  47826  sbcpr  47910  eufsnlem  49229  iscnrm3lem2  49323  functhincfun  49837  termcarweu  49916  setrec2fun  50080  elsetrecslem  50087  setrecsss  50089  setrecsres  50090  0setrec  50092  pgindnf  50104