Theorem alrimiv 1957

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem is used by:  alrimivv  1958  cbvalivw  2037  aevlem0  2086  aev  2089  aev2  2090  stdpc4  2102  sbimdv  2112  sbbidv  2113  elequ2g  2159  cbv3v2  2277  nexmo  2569  moimdv  2574  mobidv  2577  eubidv  2614  euequ  2625  eqrdv  2761  abbidv  2829  elex22  3479  pm13.183  3625  moeq3  3675  sbc2or  3753  sbcthdv  3760  csbied  3889  ssrdv  3943  eq0rdv  4372  rabeqsnd  4635  rabsn  4687  dfnfc2  4894  intab  4943  iuneq12df  4983  elALT2  5340  reusv2lem1  5369  reusv2lem2  5370  axprlem3OLD  5400  sbcop1  5470  euotd  5496  ssrelrel  5782  relimasn  6087  asymref2  6117  dfpo2  6297  iotaval2  6507  iota5  6519  iotabidv  6520  funmo  6552  funco  6576  funun  6582  fununfun  6584  fununi  6611  nfunsn  6920  fvn0ssdmfun  7069  f1oresrab  7123  0mpo0  7493  funoprabg  7531  tfisi  7851  limom  7874  funcnvuni  7925  1stconst  8091  2ndconst  8092  frxp  8118  fnwelem  8123  frxp2  8136  frxp3  8143  frrlem9  8287  seqomlem2  8434  iserd  8717  fsetdmprc0  8848  ssfi  9153  findcard3  9239  frfi  9241  fiint  9282  dffi2  9379  hartogslem1  9500  wdomd  9539  ixpiunwdom  9548  ttrclss  9685  ttrclselem2  9691  rankval3b  9794  fseqenlem2  10014  dfac3  10110  dfac5  10117  dfac2b  10119  dfac8  10124  dfac9  10125  dfacacn  10130  dfac13  10131  kmlem1  10139  kmlem6  10144  kmlem13  10151  fin23lem32  10332  zornn0g  10493  fpwwe2lem10  10629  fpwwe2lem11  10630  fpwwe2lem12  10631  hargch  10662  alephgch  10663  nqpr  11003  reclem2pr  11037  hashgt23el  14466  rtrclreclem4  15103  dfrtrcl2  15104  relexpindlem  15105  shftfn  15115  ramub  17077  ramcl  17093  imasaddfnlem  17586  imasvscafn  17595  mrieqv2d  17699  mreexexd  17708  invfun  17825  joinfval  18431  meetfval  18445  mreclatBAD  18623  letsr  18653  efgval  19791  efgi  19793  efgi2  19799  gsumval3lem2  19980  gsumzaddlem  19995  pgpfac1lem5  20155  ringurd  20271  zrinitorngc  20750  zrtermorngc  20751  zrtermoringc  20783  islbs3  21288  lbsextlem4  21294  rspsn0  21381  ssdifidl  21494  cssmre  21852  obslbs  21889  mplsubglem  22157  mpllsslem  22158  tgcl  23135  indistopon  23167  ppttop  23173  epttop  23175  mretopd  23258  toponmre  23259  neissex  23293  neiptoptop  23297  lmfun  23547  2ndcdisj  23622  1stccnp  23628  kgentopon  23704  dfac14  23784  ptcnp  23788  uptx  23791  ptrescn  23805  qtoptop2  23865  filconn  24049  filssufilg  24077  rnelfmlem  24118  alexsubALTlem2  24214  cnextfun  24230  utoptop  24400  prdsxmslem2  24695  vitalilem3  25778  mbfposr  25820  mbfinf  25833  i1fd  25849  itg1climres  25882  perfdvf  26071  taylf  26533  addbdaylem  28219  noseqrdgfn  28508  n0cut  28536  mpteleeOLD  29254  upgr1eopALT  29476  upgrspanop  29656  umgrspanop  29657  usgrspanop  29658  cplgrop  29796  umgr2v2enb1  29885  clwwlknon1loop  30458  wlkl0  30727  ex-natded9.26  30779  ex-natded9.26-2  30780  aevdemo  30820  nmcexi  32387  iuneq12daf  32910  iinabrex  32923  abfmpeld  33008  abfmpel  33009  ssmxidl  33766  exsslsb  33996  zarclssn  34272  bnj1143  35187  bnj1379  35227  bnj149  35272  rankval4b  35502  r1omhfb  35517  fineqvac  35537  r1omhfbregs  35558  kardval  35573  gblacfnacd  35594  vonf1wev  35600  vonf1owevOLD  35602  wevgblacfn  35603  loop1cycl  35637  satffunlem1lem1  35902  satffunlem2lem1  35904  prv0  35930  mclsssvlem  36062  ssmclslem  36065  mclsax  36069  mclsind  36070  dfon2lem6  36286  dfon2lem8  36288  dfon2lem9  36289  dfon2  36290  trer  36855  finminlem  36857  neibastop1  36898  neibastop3  36901  weiunfr  37006  axuntco  37018  regsfromunir1  37079  mh-regprimbi  37084  unbdqndv1  37125  knoppndv  37151  bj-ssbid1ALT  37315  bj-eqs  37326  bj-sb  37340  bj-substw  37378  bj-spcimdv  37558  bj-spcimdvv  37559  bj-csbprc  37573  bj-gabss  37599  bj-elgab  37603  curryset  37610  currysetlem3  37613  bj-cleq  37626  exellimddv  38019  finorwe  38056  wl-motae  38198  wl-cbvalsbi  38229  fin2so  38286  poimirlem17  38316  mblfinlem3  38338  ismblfin  38340  itg2addnc  38353  upixp  38408  mpobi123f  38839  mptbi12f  38843  preuniqval  39173  trcoss  39249  eldisjsim5  39616  prter1  39681  axc11n-16  39740  ax12eq  39743  ax12el  39744  sticksstones22  42963  sbtd  43008  sn-axprlem3  43017  sn-exelALT  43018  ismrcd1  43457  ttac  43791  fnwe2  43808  aomclem6  43814  dfac11  43817  dfac21  43821  hbtlem2  43879  oaun3lem1  44129  cllem0  44320  clss2lem  44365  mptrcllem  44367  iunrelexpmin1  44462  iunrelexpmin2  44466  iunrelexpuztr  44473  dftrcl3  44474  brtrclfv2  44481  dfrtrcl3  44487  psshepw  44542  frege91  44708  frege97  44714  frege109  44726  frege130  44747  grumnudlem  45023  ismnushort  45039  axc11next  45144  pm13.192  45148  pm14.24  45170  gen11  45353  trsspwALT2  45555  snssiALT  45564  sstrALT2  45571  en3lpVD  45581  sspwimp  45654  sspwimpcf  45656  sspwimpALT  45661  ax6e2ndeqALT  45667  ssmapsn  45960  infnsuprnmpt  45993  uzinico  46303  icccncfext  46629  itgsinexplem1  46696  sge0resplit  47148  hspdifhsp  47358  smflimsuplem7  47568  dfatcolem  48020  iccpartdisj  48214  sbcpr  48298  eufsnlem  49647  iscnrm3lem2  49741  functhincfun  50255  termcarweu  50334  setrec2fun  50498  elsetrecslem  50505  setrecsss  50507  setrecsres  50508  0setrec  50510  pgindnf  50522