Theorem alrimiv 1931

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem is referenced by:  alrimivv  1932  cbvalivw  2011  aevlem0  2058  aev  2061  aev2  2062  stdpc4  2072  sbimdv  2082  sbbidv  2083  elequ2g  2124  cbv3v2  2237  nexmo  2541  moimdv  2546  mobidv  2549  eubidv  2586  euequ  2597  eqrdv  2736  abbidv  2808  raleqbidvv  3329  elex2  3443  elex22  3444  ceqsexv  3469  pm13.183  3590  moeq3  3642  sbc2or  3720  sbcthdv  3727  sbcimdvOLD  3787  csbied  3866  ssrdv  3923  ss2abdvOLD  3995  abssdv  3998  eq0rdv  4335  disj  4378  rabsn  4654  dfnfc2  4860  intab  4906  intprg  4909  iuneq12df  4947  dfiin2g  4958  mpteq12dvaOLD  5160  el  5287  reusv2lem1  5316  reusv2lem2  5317  axprlem3  5343  sbcop1  5396  euotd  5421  ssrelrel  5695  asymref2  6011  dfpo2  6188  iotaval  6392  iota5  6401  iotabidv  6402  funmo  6434  funco  6458  funun  6464  fununfun  6466  fununi  6493  nfunsn  6793  fvn0ssdmfun  6934  f1oresrab  6981  0mpo0  7336  funoprabg  7373  tfisi  7680  limom  7703  funcnvuni  7752  1stconst  7911  2ndconst  7912  frxp  7938  fnwelem  7943  frrlem9  8081  seqomlem2  8252  iserd  8482  fsetdmprc0  8601  ssfi  8918  findcard3  8987  frfi  8989  fiint  9021  dffi2  9112  hartogslem1  9231  wdomd  9270  ixpiunwdom  9279  rankval3b  9515  fseqenlem2  9712  dfac3  9808  dfac5  9815  dfac2b  9817  dfac8  9822  dfac9  9823  dfacacn  9828  dfac13  9829  kmlem1  9837  kmlem6  9842  kmlem13  9849  fin23lem32  10031  axdc2lem  10135  zornn0g  10192  fpwwe2lem10  10327  fpwwe2lem11  10328  fpwwe2lem12  10329  hargch  10360  alephgch  10361  nqpr  10701  reclem2pr  10735  hashgt23el  14067  cshwsexa  14465  rtrclreclem4  14700  dfrtrcl2  14701  relexpindlem  14702  shftfn  14712  ramub  16642  ramcl  16658  imasaddfnlem  17156  imasvscafn  17165  mrieqv2d  17265  mreexexd  17274  invfun  17393  joinfval  18006  meetfval  18020  mreclatBAD  18196  letsr  18226  efgval  19238  efgi  19240  efgi2  19246  gsumval3lem2  19422  gsumzaddlem  19437  pgpfac1lem5  19597  islbs3  20332  lbsextlem4  20338  cssmre  20810  obslbs  20847  mplsubglem  21115  mpllsslem  21116  tgcl  22027  indistopon  22059  ppttop  22065  epttop  22067  mretopd  22151  toponmre  22152  neissex  22186  neiptoptop  22190  lmfun  22440  2ndcdisj  22515  1stccnp  22521  kgentopon  22597  dfac14  22677  ptcnp  22681  uptx  22684  ptrescn  22698  qtoptop2  22758  filconn  22942  filssufilg  22970  rnelfmlem  23011  alexsubALTlem2  23107  cnextfun  23123  utoptop  23294  prdsxmslem2  23591  vitalilem3  24679  mbfposr  24721  mbfinf  24734  i1fd  24750  itg1climres  24784  perfdvf  24972  taylf  25425  mptelee  27166  upgr1eopALT  27390  upgrspanop  27567  umgrspanop  27568  usgrspanop  27569  cplgrop  27707  umgr2v2enb1  27796  clwwlknon1loop  28363  wlkl0  28632  ex-natded9.26  28684  ex-natded9.26-2  28685  aevdemo  28725  nmcexi  30289  rabeqsnd  30749  iuneq12daf  30797  iinabrex  30809  abfmpeld  30893  abfmpel  30894  fpwrelmap  30970  rngurd  31384  ssmxidl  31544  zarclssn  31725  bnj1143  32670  bnj1379  32710  bnj149  32755  fineqvac  32966  loop1cycl  32999  satffunlem1lem1  33264  satffunlem2lem1  33266  prv0  33292  mclsssvlem  33424  ssmclslem  33427  mclsax  33431  mclsind  33432  dfon2lem6  33670  dfon2lem8  33672  dfon2lem9  33673  dfon2  33674  ttrclss  33706  ttrclselem2  33712  frxp2  33718  frxp3  33724  trer  34432  finminlem  34434  neibastop1  34475  neibastop3  34478  unbdqndv1  34615  knoppndv  34641  bj-ssbid1ALT  34773  bj-eqs  34783  bj-sb  34796  bj-substw  34831  bj-nnfbd  34835  bj-spcimdv  35007  bj-spcimdvv  35008  bj-csbprc  35022  bj-gabss  35050  bj-elgab  35054  curryset  35062  currysetlem3  35065  bj-cleq  35079  exellimddv  35443  finorwe  35480  wl-motae  35601  wl-cbvalsbi  35631  fin2so  35691  poimirlem17  35721  mblfinlem3  35743  ismblfin  35745  itg2addnc  35758  upixp  35814  mpobi123f  36247  mptbi12f  36251  trcoss  36527  prter1  36820  axc11n-16  36879  ax12eq  36882  ax12el  36883  sticksstones22  40052  sbtd  40104  sn-axprlem3  40114  sn-el  40115  sn-iotaval  40119  ismrcd1  40436  ttac  40774  fnwe2  40794  aomclem6  40800  dfac11  40803  dfac21  40807  hbtlem2  40865  cllem0  41062  clss2lem  41108  mptrcllem  41110  iunrelexpmin1  41205  iunrelexpmin2  41209  iunrelexpuztr  41216  dftrcl3  41217  brtrclfv2  41224  dfrtrcl3  41230  psshepw  41285  frege91  41451  frege97  41457  frege109  41469  frege130  41490  grumnudlem  41792  ismnushort  41808  axc11next  41913  pm13.192  41917  pm14.24  41939  gen11  42125  trsspwALT2  42328  snssiALT  42337  sstrALT2  42344  en3lpVD  42354  sspwimp  42427  sspwimpcf  42429  sspwimpALT  42434  ax6e2ndeqALT  42440  ssmapsn  42645  infnsuprnmpt  42685  uzinico  42988  icccncfext  43318  itgsinexplem1  43385  sge0resplit  43834  hoidmvlelem1  44023  hspdifhsp  44044  smflimsuplem7  44246  dfatcolem  44634  iccpartdisj  44777  sbcpr  44861  zrinitorngc  45446  zrtermorngc  45447  zrtermoringc  45516  eufsnlem  46056  iscnrm3lem2  46116  setrec2fun  46284  elsetrecslem  46290  setrecsss  46292  setrecsres  46293  0setrec  46295