Theorem alrimiv 1960

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2244 and 19.21v 1972. (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 1943	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alrimiv.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	alrimih 1857	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 1828  ax-4 1842  ax-5 1943

This theorem is used by:  alrimivv  1961  cbvalivw  2040  aevlem0  2089  aev  2092  aev2  2093  stdpc4  2105  sbimdv  2115  sbbidv  2116  elequ2g  2161  cbv3v2  2278  nexmo  2567  moimdv  2572  mobidv  2575  eubidv  2612  euequ  2623  eqrdv  2759  abbidv  2827  elex22  3475  pm13.183  3620  moeq3  3670  sbc2or  3748  sbcthdv  3755  csbied  3883  ssrdv  3937  eq0rdv  4365  rabeqsnd  4630  rabsn  4682  dfnfc2  4889  intab  4938  iuneq12df  4978  elALT2  5331  reusv2lem1  5360  reusv2lem2  5361  sbcop1  5458  euotd  5486  ssrelrel  5772  relimasn  6083  asymref2  6111  dfpo2  6299  iotaval2  6509  iota5  6521  iotabidv  6522  funmo  6554  funco  6580  funun  6586  fununfun  6588  fununi  6615  nfunsn  6924  fvn0ssdmfun  7074  f1oresrab  7128  0mpo0  7503  funoprabg  7541  tfisi  7870  limom  7893  funcnvuni  7944  1stconst  8111  2ndconst  8112  frxp  8138  fnwelem  8143  fnwe2  8149  frxp2  8161  frxp3  8168  frrlem9  8312  seqomlem2  8461  iserd  8744  fsetdmprc0  8877  ssfi  9188  findcard3  9274  frfi  9276  fiint  9318  dffi2  9415  hartogslem1  9536  wdomd  9575  ixpiunwdom  9584  ttrclss  9721  ttrclselem2  9727  rankval3b  9836  rankval4b  9880  hfpw  9926  setrec2fun  9973  fseqenlem2  10104  dfac3  10200  dfac5  10207  dfac2b  10209  dfac8  10214  dfac9  10215  dfacacn  10220  dfac13  10221  kmlem1  10229  kmlem6  10234  kmlem13  10241  fin23lem32  10422  zornn0g  10583  fpwwe2lem10  10725  fpwwe2lem11  10726  fpwwe2lem12  10727  hargch  10758  alephgch  10759  nqpr  11099  reclem2pr  11133  hashgt23el  14569  rtrclreclem4  15214  dfrtrcl2  15215  relexpindlem  15216  shftfn  15226  ramub  17191  ramcl  17207  imasaddfnlem  17700  imasvscafn  17709  mrieqv2d  17813  mreexexd  17822  invfun  17939  joinfval  18545  meetfval  18559  mreclatBAD  18737  letsr  18767  efgval  19931  efgi  19933  efgi2  19939  gsumval3lem2  20120  gsumzaddlem  20135  pgpfac1lem5  20295  ringurd  20411  zrinitorngc  20894  zrtermorngc  20895  zrtermoringc  20927  islbs3  21433  lbsextlem4  21439  rspsn0  21526  ssdifidl  21641  cssmre  21999  obslbs  22036  mplsubglem  22306  mpllsslem  22307  tgcl  23287  indistopon  23319  ppttop  23325  epttop  23327  mretopd  23410  toponmre  23411  neissex  23445  neiptoptop  23449  lmfun  23699  2ndcdisj  23775  1stccnp  23781  kgentopon  23857  dfac14  23937  ptcnp  23941  uptx  23944  ptrescn  23958  qtoptop2  24018  filconn  24202  filssufilg  24230  rnelfmlem  24271  alexsubALTlem2  24367  cnextfun  24383  utoptop  24553  prdsxmslem2  24848  vitalilem3  25931  mbfposr  25973  mbfinf  25986  i1fd  26002  itg1climres  26035  perfdvf  26223  taylf  26688  addbdaylem  28403  noseqrdgfn  28692  n0cut  28720  mpteleeOLD  29473  upgr1eopALT  29695  upgrspanop  29878  umgrspanop  29879  usgrspanop  29880  cplgrop  30018  umgr2v2enb1  30107  clwwlknon1loop  30689  loop1cycl  30744  wlkl0  30968  ex-natded9.26  31020  ex-natded9.26-2  31021  aevdemo  31061  nmcexi  32628  iuneq12daf  33151  iinabrex  33163  abfmpeld  33248  abfmpel  33249  ssmxidl  33999  exsslsb  34229  zarclssn  34505  bnj1143  35420  bnj1379  35460  bnj149  35505  r1omhfb  35738  fineqvac  35784  r1omhfbregs  35805  kardval  35820  gblacfnacd  35881  vonf1wev  35887  vonf1owevOLD  35889  wevgblacfn  35890  vonf1onprcf1ac  35894  onprcf1acwevdlem2  35896  satffunlem1lem1  36167  satffunlem2lem1  36169  prv0  36195  mclsssvlem  36327  ssmclslem  36330  mclsax  36334  mclsind  36335  dfon2lem6  36550  dfon2lem8  36552  dfon2lem9  36553  dfon2  36554  trer  37104  finminlem  37106  neibastop1  37147  neibastop3  37150  weiunfr  37255  axuntco  37267  regsfromunir1  37328  mh-regprimbi  37333  unbdqndv1  37374  knoppndv  37400  bj-ssbid1ALT  37564  bj-eqs  37575  bj-sb  37589  bj-substw  37627  bj-spcimdv  37807  bj-spcimdvv  37808  bj-csbprc  37822  bj-gabss  37848  bj-elgab  37852  curryset  37859  currysetlem3  37862  bj-cleq  37875  exellimddv  38268  finorwe  38305  wl-motae  38447  wl-cbvalsbi  38478  fin2so  38530  poimirlem17  38555  mblfinlem3  38577  ismblfin  38579  itg2addnc  38592  findcard4  38632  varprop  38642  negprop  38643  impprop  38644  upixp  38663  mpobi123f  39094  mptbi12f  39098  preuniqval  39428  trcoss  39504  eldisjsim5  39871  prter1  39936  axc11n-16  39995  ax12eq  39998  ax12el  39999  sticksstones22  43218  sbtd  43263  sn-axprlem3  43272  sn-exelALT  43273  ismrcd1  43708  ttac  44042  aomclem6  44060  dfac11  44063  dfac21  44067  hbtlem2  44125  oaun3lem1  44375  cllem0  44566  clss2lem  44610  mptrcllem  44612  iunrelexpmin1  44707  iunrelexpmin2  44711  iunrelexpuztr  44718  dftrcl3  44719  brtrclfv2  44726  dfrtrcl3  44732  psshepw  44787  frege91  44953  frege97  44959  frege109  44971  frege130  44992  grumnudlem  45268  ismnushort  45284  axc11next  45389  pm13.192  45393  pm14.24  45415  gen11  45598  trsspwALT2  45800  snssiALT  45809  sstrALT2  45816  en3lpVD  45826  sspwimp  45899  sspwimpcf  45901  sspwimpALT  45906  ax6e2ndeqALT  45912  ssmapsn  46228  infnsuprnmpt  46261  uzinico  46570  icccncfext  46896  itgsinexplem1  46963  sge0resplit  47415  hspdifhsp  47625  smflimsuplem7  47835  dfatcolem  48324  iccpartdisj  48518  sbcpr  48602  eufsnlem  49950  iscnrm3lem2  50042  functhincfun  50556  termcarweu  50635  elsetrecslem  50791  setrecsss  50793  setrecsres  50794  0setrec  50796  pgindnf  50808