Theorem alrimiv 1927

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  alrimivv  1928  cbvalivw  2007  aevlem0  2055  aev  2058  aev2  2059  stdpc4  2069  sbimdv  2079  sbbidv  2080  elequ2g  2125  cbv3v2  2242  nexmo  2534  moimdv  2539  mobidv  2542  eubidv  2579  euequ  2590  eqrdv  2727  abbidv  2795  raleqbidvvOLD  3305  elex22  3469  pm13.183  3629  moeq3  3680  sbc2or  3759  sbcthdv  3766  csbied  3895  ssrdv  3949  eq0rdv  4366  disj  4409  rabeqsnd  4629  rabsn  4681  dfnfc2  4889  intab  4938  intprg  4941  iuneq12df  4978  dfiin2g  4991  abexd  5275  elALT2  5319  reusv2lem1  5348  reusv2lem2  5349  axprlem3OLD  5378  sbcop1  5443  euotd  5468  ssrelrel  5750  asymref2  6078  dfpo2  6257  iotaval2  6467  iotavalOLD  6473  iota5  6482  iotabidv  6483  funmo  6516  funco  6540  funun  6546  fununfun  6548  fununi  6575  nfunsn  6882  fvn0ssdmfun  7028  f1oresrab  7081  0mpo0  7452  funoprabg  7490  tfisi  7815  limom  7838  funcnvuni  7888  1stconst  8056  2ndconst  8057  frxp  8082  fnwelem  8087  frxp2  8100  frxp3  8107  frrlem9  8250  seqomlem2  8396  iserd  8674  fsetdmprc0  8805  ssfi  9114  findcard3  9205  findcard3OLD  9206  frfi  9208  fiint  9253  fiintOLD  9254  dffi2  9350  hartogslem1  9471  wdomd  9510  ixpiunwdom  9519  ttrclss  9649  ttrclselem2  9655  rankval3b  9755  fseqenlem2  9954  dfac3  10050  dfac5  10058  dfac2b  10060  dfac8  10065  dfac9  10066  dfacacn  10071  dfac13  10072  kmlem1  10080  kmlem6  10085  kmlem13  10092  fin23lem32  10273  axdc2lem  10377  zornn0g  10434  fpwwe2lem10  10569  fpwwe2lem11  10570  fpwwe2lem12  10571  hargch  10602  alephgch  10603  nqpr  10943  reclem2pr  10977  hashgt23el  14365  cshwsexaOLD  14766  rtrclreclem4  15003  dfrtrcl2  15004  relexpindlem  15005  shftfn  15015  ramub  16960  ramcl  16976  imasaddfnlem  17467  imasvscafn  17476  mrieqv2d  17580  mreexexd  17589  invfun  17706  joinfval  18312  meetfval  18326  mreclatBAD  18504  letsr  18534  efgval  19631  efgi  19633  efgi2  19639  gsumval3lem2  19820  gsumzaddlem  19835  pgpfac1lem5  19995  ringurd  20105  zrinitorngc  20562  zrtermorngc  20563  zrtermoringc  20595  islbs3  21097  lbsextlem4  21103  cssmre  21635  obslbs  21672  mplsubglem  21941  mpllsslem  21942  tgcl  22889  indistopon  22921  ppttop  22927  epttop  22929  mretopd  23012  toponmre  23013  neissex  23047  neiptoptop  23051  lmfun  23301  2ndcdisj  23376  1stccnp  23382  kgentopon  23458  dfac14  23538  ptcnp  23542  uptx  23545  ptrescn  23559  qtoptop2  23619  filconn  23803  filssufilg  23831  rnelfmlem  23872  alexsubALTlem2  23968  cnextfun  23984  utoptop  24155  prdsxmslem2  24450  vitalilem3  25544  mbfposr  25586  mbfinf  25599  i1fd  25615  itg1climres  25648  perfdvf  25837  taylf  26301  addsbdaylem  27963  noseqrdgfn  28240  n0scut  28266  mptelee  28875  upgr1eopALT  29097  upgrspanop  29277  umgrspanop  29278  usgrspanop  29279  cplgrop  29417  umgr2v2enb1  29507  clwwlknon1loop  30077  wlkl0  30346  ex-natded9.26  30398  ex-natded9.26-2  30399  aevdemo  30439  nmcexi  32005  iuneq12daf  32535  iinabrex  32548  abfmpeld  32628  abfmpel  32629  fpwrelmap  32706  ssdifidl  33421  ssmxidl  33438  exsslsb  33585  zarclssn  33856  bnj1143  34773  bnj1379  34813  bnj149  34858  fineqvac  35080  gblacfnacd  35082  vonf1owev  35088  wevgblacfn  35089  loop1cycl  35117  satffunlem1lem1  35382  satffunlem2lem1  35384  prv0  35410  mclsssvlem  35542  ssmclslem  35545  mclsax  35549  mclsind  35550  dfon2lem6  35769  dfon2lem8  35771  dfon2lem9  35772  dfon2  35773  trer  36297  finminlem  36299  neibastop1  36340  neibastop3  36343  weiunfr  36448  unbdqndv1  36489  knoppndv  36515  bj-ssbid1ALT  36646  bj-eqs  36656  bj-sb  36668  bj-substw  36703  bj-nnfbd  36707  bj-spcimdv  36876  bj-spcimdvv  36877  bj-csbprc  36891  bj-gabss  36916  bj-elgab  36920  curryset  36927  currysetlem3  36930  bj-cleq  36943  exellimddv  37326  finorwe  37363  wl-motae  37496  wl-cbvalsbi  37527  fin2so  37594  poimirlem17  37624  mblfinlem3  37646  ismblfin  37648  itg2addnc  37661  upixp  37716  mpobi123f  38149  mptbi12f  38153  trcoss  38466  prter1  38865  axc11n-16  38924  ax12eq  38927  ax12el  38928  sticksstones22  42149  sbtd  42192  sn-axprlem3  42198  sn-exelALT  42199  ismrcd1  42679  ttac  43018  fnwe2  43035  aomclem6  43041  dfac11  43044  dfac21  43048  hbtlem2  43106  oaun3lem1  43356  cllem0  43548  clss2lem  43593  mptrcllem  43595  iunrelexpmin1  43690  iunrelexpmin2  43694  iunrelexpuztr  43701  dftrcl3  43702  brtrclfv2  43709  dfrtrcl3  43715  psshepw  43770  frege91  43936  frege97  43942  frege109  43954  frege130  43975  grumnudlem  44267  ismnushort  44283  axc11next  44388  pm13.192  44392  pm14.24  44414  gen11  44599  trsspwALT2  44801  snssiALT  44810  sstrALT2  44817  en3lpVD  44827  sspwimp  44900  sspwimpcf  44902  sspwimpALT  44907  ax6e2ndeqALT  44913  ssmapsn  45203  infnsuprnmpt  45237  uzinico  45550  icccncfext  45878  itgsinexplem1  45945  sge0resplit  46397  hoidmvlelem1  46586  hspdifhsp  46607  smflimsuplem7  46817  dfatcolem  47249  iccpartdisj  47431  sbcpr  47515  eufsnlem  48822  iscnrm3lem2  48916  functhincfun  49431  termcarweu  49510  setrec2fun  49674  elsetrecslem  49681  setrecsss  49683  setrecsres  49684  0setrec  49686  pgindnf  49698