Theorem alrimiv 1954

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

Syntax hints:   → wi 4  ∀wal 1565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem is referenced by:  alrimivv  1955  cbvalivw  2034  aevlem0  2083  aev  2086  aev2  2087  stdpc4lem  2104  stdpc4ALT  2106  sbimdv  2118  sbbidv  2119  elequ2g  2165  cbv3v2  2283  nexmo  2575  moimdv  2580  mobidv  2583  eubidv  2620  euequ  2631  eqrdv  2767  abbidv  2835  elex22  3487  pm13.183  3634  moeq3  3684  sbc2or  3762  sbcthdv  3769  csbied  3897  ssrdv  3951  eq0rdv  4378  rabeqsnd  4640  rabsn  4692  dfnfc2  4898  intab  4947  iuneq12df  4987  elALT2  5341  reusv2lem1  5370  reusv2lem2  5371  axprlem3OLD  5401  sbcop1  5471  euotd  5497  ssrelrel  5783  relimasn  6088  asymref2  6118  dfpo2  6298  iotaval2  6508  iota5  6520  iotabidv  6521  funmo  6553  funco  6577  funun  6583  fununfun  6585  fununi  6612  nfunsn  6921  fvn0ssdmfun  7070  f1oresrab  7124  0mpo0  7494  funoprabg  7532  tfisi  7855  limom  7878  funcnvuni  7929  1stconst  8095  2ndconst  8096  frxp  8122  fnwelem  8127  frxp2  8140  frxp3  8147  frrlem9  8291  seqomlem2  8438  iserd  8721  fsetdmprc0  8852  ssfi  9157  findcard3  9243  frfi  9245  fiint  9286  dffi2  9383  hartogslem1  9504  wdomd  9543  ixpiunwdom  9552  ttrclss  9689  ttrclselem2  9695  rankval3b  9798  fseqenlem2  10009  dfac3  10105  dfac5  10112  dfac2b  10114  dfac8  10119  dfac9  10120  dfacacn  10125  dfac13  10126  kmlem1  10134  kmlem6  10139  kmlem13  10146  fin23lem32  10328  zornn0g  10489  fpwwe2lem10  10625  fpwwe2lem11  10626  fpwwe2lem12  10627  hargch  10658  alephgch  10659  nqpr  10999  reclem2pr  11033  hashgt23el  14461  rtrclreclem4  15098  dfrtrcl2  15099  relexpindlem  15100  shftfn  15110  ramub  17073  ramcl  17089  imasaddfnlem  17582  imasvscafn  17591  mrieqv2d  17695  mreexexd  17704  invfun  17821  joinfval  18427  meetfval  18441  mreclatBAD  18619  letsr  18649  efgval  19787  efgi  19789  efgi2  19795  gsumval3lem2  19976  gsumzaddlem  19991  pgpfac1lem5  20151  ringurd  20267  zrinitorngc  20727  zrtermorngc  20728  zrtermoringc  20760  islbs3  21257  lbsextlem4  21263  ssdifidl  21454  cssmre  21812  obslbs  21849  mplsubglem  22117  mpllsslem  22118  tgcl  23095  indistopon  23127  ppttop  23133  epttop  23135  mretopd  23218  toponmre  23219  neissex  23253  neiptoptop  23257  lmfun  23507  2ndcdisj  23582  1stccnp  23588  kgentopon  23664  dfac14  23744  ptcnp  23748  uptx  23751  ptrescn  23765  qtoptop2  23825  filconn  24009  filssufilg  24037  rnelfmlem  24078  alexsubALTlem2  24174  cnextfun  24190  utoptop  24360  prdsxmslem2  24655  vitalilem3  25738  mbfposr  25780  mbfinf  25793  i1fd  25809  itg1climres  25842  perfdvf  26031  taylf  26490  addbdaylem  28176  noseqrdgfn  28465  n0cut  28493  mpteleeOLD  29186  upgr1eopALT  29408  upgrspanop  29588  umgrspanop  29589  usgrspanop  29590  cplgrop  29728  umgr2v2enb1  29817  clwwlknon1loop  30390  wlkl0  30659  ex-natded9.26  30711  ex-natded9.26-2  30712  aevdemo  30752  nmcexi  32319  iuneq12daf  32842  iinabrex  32855  abfmpeld  32940  abfmpel  32941  ssmxidl  33702  exsslsb  33932  zarclssn  34208  bnj1143  35123  bnj1379  35163  bnj149  35208  rankval4b  35436  r1omhfb  35449  fineqvac  35462  r1omhfbregs  35483  kardval  35498  gblacfnacd  35519  vonf1wev  35525  vonf1owevOLD  35527  wevgblacfn  35528  loop1cycl  35562  satffunlem1lem1  35827  satffunlem2lem1  35829  prv0  35855  mclsssvlem  35987  ssmclslem  35990  mclsax  35994  mclsind  35995  dfon2lem6  36211  dfon2lem8  36213  dfon2lem9  36214  dfon2  36215  trer  36750  finminlem  36752  neibastop1  36793  neibastop3  36796  weiunfr  36901  axuntco  36913  regsfromunir1  36974  mh-regprimbi  36979  unbdqndv1  37020  knoppndv  37046  bj-ssbid1ALT  37210  bj-eqs  37221  bj-sb  37235  bj-substw  37273  bj-spcimdv  37453  bj-spcimdvv  37454  bj-csbprc  37468  bj-gabss  37493  bj-elgab  37497  curryset  37504  currysetlem3  37507  bj-cleq  37520  exellimddv  37913  finorwe  37950  wl-motae  38092  wl-cbvalsbi  38123  fin2so  38180  poimirlem17  38210  mblfinlem3  38232  ismblfin  38234  itg2addnc  38247  upixp  38302  mpobi123f  38735  mptbi12f  38739  preuniqval  39069  trcoss  39145  eldisjsim5  39512  prter1  39577  axc11n-16  39636  ax12eq  39639  ax12el  39640  sticksstones22  42859  sbtd  42904  sn-axprlem3  42913  sn-exelALT  42914  ismrcd1  43355  ttac  43689  fnwe2  43706  aomclem6  43712  dfac11  43715  dfac21  43719  hbtlem2  43777  oaun3lem1  44027  cllem0  44218  clss2lem  44263  mptrcllem  44265  iunrelexpmin1  44360  iunrelexpmin2  44364  iunrelexpuztr  44371  dftrcl3  44372  brtrclfv2  44379  dfrtrcl3  44385  psshepw  44440  frege91  44606  frege97  44612  frege109  44624  frege130  44645  grumnudlem  44921  ismnushort  44937  axc11next  45042  pm13.192  45046  pm14.24  45068  gen11  45251  trsspwALT2  45453  snssiALT  45462  sstrALT2  45469  en3lpVD  45479  sspwimp  45552  sspwimpcf  45554  sspwimpALT  45559  ax6e2ndeqALT  45565  ssmapsn  45858  infnsuprnmpt  45891  uzinico  46201  icccncfext  46527  itgsinexplem1  46594  sge0resplit  47046  hspdifhsp  47256  smflimsuplem7  47466  dfatcolem  47915  iccpartdisj  48109  sbcpr  48193  eufsnlem  49538  iscnrm3lem2  49632  functhincfun  50146  termcarweu  50225  setrec2fun  50389  elsetrecslem  50396  setrecsss  50398  setrecsres  50399  0setrec  50401  pgindnf  50413