Theorem alrimiv 1931

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2201 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 1798  ax-4 1812  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  2123  cbv3v2  2235  nexmo  2542  moimdv  2547  mobidv  2550  eubidv  2587  euequ  2598  eqrdv  2737  abbidv  2808  raleqbidvv  3339  elex2OLD  3454  elex22  3455  ceqsexv  3480  pm13.183  3598  moeq3  3648  sbc2or  3726  sbcthdv  3733  sbcimdvOLD  3792  csbied  3871  ssrdv  3928  ss2abdvOLD  4000  abssdv  4003  eq0rdv  4339  disj  4382  rabsn  4658  dfnfc2  4864  intab  4910  intprg  4913  iuneq12df  4951  dfiin2g  4963  mpteq12dvaOLD  5165  elALT2  5293  reusv2lem1  5322  reusv2lem2  5323  axprlem3  5349  sbcop1  5403  euotd  5428  ssrelrel  5708  asymref2  6027  dfpo2  6203  iotaval  6411  iota5  6420  iotabidv  6421  funmo  6456  funmoOLD  6457  funco  6481  funun  6487  fununfun  6489  fununi  6516  nfunsn  6820  fvn0ssdmfun  6961  f1oresrab  7008  0mpo0  7367  funoprabg  7404  tfisi  7714  limom  7737  funcnvuni  7787  1stconst  7949  2ndconst  7950  frxp  7976  fnwelem  7981  frrlem9  8119  seqomlem2  8291  iserd  8533  fsetdmprc0  8652  ssfi  8965  findcard3  9066  frfi  9068  fiint  9100  dffi2  9191  hartogslem1  9310  wdomd  9349  ixpiunwdom  9358  ttrclss  9487  ttrclselem2  9493  rankval3b  9593  fseqenlem2  9790  dfac3  9886  dfac5  9893  dfac2b  9895  dfac8  9900  dfac9  9901  dfacacn  9906  dfac13  9907  kmlem1  9915  kmlem6  9920  kmlem13  9927  fin23lem32  10109  axdc2lem  10213  zornn0g  10270  fpwwe2lem10  10405  fpwwe2lem11  10406  fpwwe2lem12  10407  hargch  10438  alephgch  10439  nqpr  10779  reclem2pr  10813  hashgt23el  14148  cshwsexa  14546  rtrclreclem4  14781  dfrtrcl2  14782  relexpindlem  14783  shftfn  14793  ramub  16723  ramcl  16739  imasaddfnlem  17248  imasvscafn  17257  mrieqv2d  17357  mreexexd  17366  invfun  17485  joinfval  18100  meetfval  18114  mreclatBAD  18290  letsr  18320  efgval  19332  efgi  19334  efgi2  19340  gsumval3lem2  19516  gsumzaddlem  19531  pgpfac1lem5  19691  islbs3  20426  lbsextlem4  20432  cssmre  20907  obslbs  20946  mplsubglem  21214  mpllsslem  21215  tgcl  22128  indistopon  22160  ppttop  22166  epttop  22168  mretopd  22252  toponmre  22253  neissex  22287  neiptoptop  22291  lmfun  22541  2ndcdisj  22616  1stccnp  22622  kgentopon  22698  dfac14  22778  ptcnp  22782  uptx  22785  ptrescn  22799  qtoptop2  22859  filconn  23043  filssufilg  23071  rnelfmlem  23112  alexsubALTlem2  23208  cnextfun  23224  utoptop  23395  prdsxmslem2  23694  vitalilem3  24783  mbfposr  24825  mbfinf  24838  i1fd  24854  itg1climres  24888  perfdvf  25076  taylf  25529  mptelee  27272  upgr1eopALT  27496  upgrspanop  27673  umgrspanop  27674  usgrspanop  27675  cplgrop  27813  umgr2v2enb1  27902  clwwlknon1loop  28471  wlkl0  28740  ex-natded9.26  28792  ex-natded9.26-2  28793  aevdemo  28833  nmcexi  30397  rabeqsnd  30857  iuneq12daf  30905  iinabrex  30917  abfmpeld  31000  abfmpel  31001  fpwrelmap  31077  rngurd  31491  ssmxidl  31651  zarclssn  31832  bnj1143  32779  bnj1379  32819  bnj149  32864  fineqvac  33075  loop1cycl  33108  satffunlem1lem1  33373  satffunlem2lem1  33375  prv0  33401  mclsssvlem  33533  ssmclslem  33536  mclsax  33540  mclsind  33541  dfon2lem6  33773  dfon2lem8  33775  dfon2lem9  33776  dfon2  33777  frxp2  33800  frxp3  33806  trer  34514  finminlem  34516  neibastop1  34557  neibastop3  34560  unbdqndv1  34697  knoppndv  34723  bj-ssbid1ALT  34855  bj-eqs  34865  bj-sb  34878  bj-substw  34913  bj-nnfbd  34917  bj-spcimdv  35089  bj-spcimdvv  35090  bj-csbprc  35104  bj-gabss  35132  bj-elgab  35136  curryset  35144  currysetlem3  35147  bj-cleq  35161  exellimddv  35525  finorwe  35562  wl-motae  35683  wl-cbvalsbi  35713  fin2so  35773  poimirlem17  35803  mblfinlem3  35825  ismblfin  35827  itg2addnc  35840  upixp  35896  mpobi123f  36329  mptbi12f  36333  trcoss  36607  prter1  36900  axc11n-16  36959  ax12eq  36962  ax12el  36963  sticksstones22  40131  sbtd  40183  sn-axprlem3  40193  sn-el  40194  iotavallem  40199  ismrcd1  40527  ttac  40865  fnwe2  40885  aomclem6  40891  dfac11  40894  dfac21  40898  hbtlem2  40956  cllem0  41180  clss2lem  41226  mptrcllem  41228  iunrelexpmin1  41323  iunrelexpmin2  41327  iunrelexpuztr  41334  dftrcl3  41335  brtrclfv2  41342  dfrtrcl3  41348  psshepw  41403  frege91  41569  frege97  41575  frege109  41587  frege130  41608  grumnudlem  41910  ismnushort  41926  axc11next  42031  pm13.192  42035  pm14.24  42057  gen11  42243  trsspwALT2  42446  snssiALT  42455  sstrALT2  42462  en3lpVD  42472  sspwimp  42545  sspwimpcf  42547  sspwimpALT  42552  ax6e2ndeqALT  42558  ssmapsn  42763  infnsuprnmpt  42803  uzinico  43105  icccncfext  43435  itgsinexplem1  43502  sge0resplit  43951  hoidmvlelem1  44140  hspdifhsp  44161  smflimsuplem7  44370  dfatcolem  44758  iccpartdisj  44900  sbcpr  44984  zrinitorngc  45569  zrtermorngc  45570  zrtermoringc  45639  eufsnlem  46179  iscnrm3lem2  46239  setrec2fun  46409  elsetrecslem  46415  setrecsss  46417  setrecsres  46418  0setrec  46420