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  3306  elex22  3466  pm13.183  3621  moeq3  3671  sbc2or  3750  sbcthdv  3757  csbied  3886  ssrdv  3940  eq0rdv  4360  rabeqsnd  4627  rabsn  4679  dfnfc2  4886  intab  4934  intprg  4937  iuneq12df  4974  dfiin2g  4987  elALT2  5315  reusv2lem1  5344  reusv2lem2  5345  axprlem3OLD  5374  sbcop1  5437  euotd  5462  ssrelrel  5746  relimasn  6045  asymref2  6075  dfpo2  6255  iotaval2  6464  iota5  6476  iotabidv  6477  funmo  6509  funco  6533  funun  6539  fununfun  6541  fununi  6568  nfunsn  6874  fvn0ssdmfun  7021  f1oresrab  7074  0mpo0  7443  funoprabg  7481  tfisi  7803  limom  7826  funcnvuni  7876  1stconst  8044  2ndconst  8045  frxp  8070  fnwelem  8075  frxp2  8088  frxp3  8095  frrlem9  8238  seqomlem2  8384  iserd  8664  fsetdmprc0  8796  ssfi  9101  findcard3  9187  frfi  9189  fiint  9231  dffi2  9330  hartogslem1  9451  wdomd  9490  ixpiunwdom  9499  ttrclss  9633  ttrclselem2  9639  rankval3b  9742  fseqenlem2  9939  dfac3  10035  dfac5  10043  dfac2b  10045  dfac8  10050  dfac9  10051  dfacacn  10056  dfac13  10057  kmlem1  10065  kmlem6  10070  kmlem13  10077  fin23lem32  10258  zornn0g  10419  fpwwe2lem10  10555  fpwwe2lem11  10556  fpwwe2lem12  10557  hargch  10588  alephgch  10589  nqpr  10929  reclem2pr  10963  hashgt23el  14351  rtrclreclem4  14988  dfrtrcl2  14989  relexpindlem  14990  shftfn  15000  ramub  16945  ramcl  16961  imasaddfnlem  17453  imasvscafn  17462  mrieqv2d  17566  mreexexd  17575  invfun  17692  joinfval  18298  meetfval  18312  mreclatBAD  18490  letsr  18520  efgval  19650  efgi  19652  efgi2  19658  gsumval3lem2  19839  gsumzaddlem  19854  pgpfac1lem5  20014  ringurd  20124  zrinitorngc  20579  zrtermorngc  20580  zrtermoringc  20612  islbs3  21114  lbsextlem4  21120  cssmre  21652  obslbs  21689  mplsubglem  21958  mpllsslem  21959  tgcl  22917  indistopon  22949  ppttop  22955  epttop  22957  mretopd  23040  toponmre  23041  neissex  23075  neiptoptop  23079  lmfun  23329  2ndcdisj  23404  1stccnp  23410  kgentopon  23486  dfac14  23566  ptcnp  23570  uptx  23573  ptrescn  23587  qtoptop2  23647  filconn  23831  filssufilg  23859  rnelfmlem  23900  alexsubALTlem2  23996  cnextfun  24012  utoptop  24182  prdsxmslem2  24477  vitalilem3  25571  mbfposr  25613  mbfinf  25626  i1fd  25642  itg1climres  25675  perfdvf  25864  taylf  26328  addbdaylem  28017  noseqrdgfn  28306  n0cut  28334  mpteleeOLD  28972  upgr1eopALT  29194  upgrspanop  29374  umgrspanop  29375  usgrspanop  29376  cplgrop  29514  umgr2v2enb1  29604  clwwlknon1loop  30177  wlkl0  30446  ex-natded9.26  30498  ex-natded9.26-2  30499  aevdemo  30539  nmcexi  32105  iuneq12daf  32634  iinabrex  32647  abfmpeld  32735  abfmpel  32736  ssdifidl  33540  ssmxidl  33557  exsslsb  33755  zarclssn  34032  bnj1143  34948  bnj1379  34988  bnj149  35033  rankval4b  35258  r1omhfb  35270  fineqvac  35274  r1omhfbregs  35295  gblacfnacd  35298  vonf1owev  35304  wevgblacfn  35305  loop1cycl  35333  satffunlem1lem1  35598  satffunlem2lem1  35600  prv0  35626  mclsssvlem  35758  ssmclslem  35761  mclsax  35765  mclsind  35766  dfon2lem6  35982  dfon2lem8  35984  dfon2lem9  35985  dfon2  35986  trer  36512  finminlem  36514  neibastop1  36555  neibastop3  36558  weiunfr  36663  exeltr  36667  regsfromunir1  36672  unbdqndv1  36710  knoppndv  36736  bj-ssbid1ALT  36868  bj-eqs  36878  bj-sb  36890  bj-substw  36925  bj-nnfbd  36929  bj-spcimdv  37098  bj-spcimdvv  37099  bj-csbprc  37113  bj-gabss  37138  bj-elgab  37142  curryset  37149  currysetlem3  37152  bj-cleq  37165  exellimddv  37552  finorwe  37589  wl-motae  37722  wl-cbvalsbi  37753  fin2so  37810  poimirlem17  37840  mblfinlem3  37862  ismblfin  37864  itg2addnc  37877  upixp  37932  mpobi123f  38365  mptbi12f  38369  preuniqval  38699  trcoss  38775  eldisjsim5  39142  prter1  39207  axc11n-16  39266  ax12eq  39269  ax12el  39270  sticksstones22  42490  sbtd  42533  sn-axprlem3  42542  sn-exelALT  42543  ismrcd1  43007  ttac  43345  fnwe2  43362  aomclem6  43368  dfac11  43371  dfac21  43375  hbtlem2  43433  oaun3lem1  43683  cllem0  43874  clss2lem  43919  mptrcllem  43921  iunrelexpmin1  44016  iunrelexpmin2  44020  iunrelexpuztr  44027  dftrcl3  44028  brtrclfv2  44035  dfrtrcl3  44041  psshepw  44096  frege91  44262  frege97  44268  frege109  44280  frege130  44301  grumnudlem  44593  ismnushort  44609  axc11next  44714  pm13.192  44718  pm14.24  44740  gen11  44924  trsspwALT2  45126  snssiALT  45135  sstrALT2  45142  en3lpVD  45152  sspwimp  45225  sspwimpcf  45227  sspwimpALT  45232  ax6e2ndeqALT  45238  ssmapsn  45527  infnsuprnmpt  45561  uzinico  45872  icccncfext  46198  itgsinexplem1  46265  sge0resplit  46717  hspdifhsp  46927  smflimsuplem7  47137  dfatcolem  47568  iccpartdisj  47750  sbcpr  47834  eufsnlem  49153  iscnrm3lem2  49247  functhincfun  49761  termcarweu  49840  setrec2fun  50004  elsetrecslem  50011  setrecsss  50013  setrecsres  50014  0setrec  50016  pgindnf  50028