Theorem alrimiv 1960

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2243 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  2277  nexmo  2566  moimdv  2571  mobidv  2574  eubidv  2611  euequ  2622  eqrdv  2758  abbidv  2826  elex22  3474  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  5334  reusv2lem1  5363  reusv2lem2  5364  axprlem3OLD  5394  sbcop1  5464  euotd  5490  ssrelrel  5776  relimasn  6081  asymref2  6111  dfpo2  6294  iotaval2  6504  iota5  6516  iotabidv  6517  funmo  6549  funco  6574  funun  6580  fununfun  6582  fununi  6609  nfunsn  6918  fvn0ssdmfun  7068  f1oresrab  7122  0mpo0  7497  funoprabg  7535  tfisi  7856  limom  7879  funcnvuni  7930  1stconst  8098  2ndconst  8099  frxp  8125  fnwelem  8130  frxp2  8143  frxp3  8150  frrlem9  8294  seqomlem2  8443  iserd  8726  fsetdmprc0  8859  ssfi  9170  findcard3  9256  frfi  9258  fiint  9299  dffi2  9396  hartogslem1  9517  wdomd  9556  ixpiunwdom  9565  ttrclss  9702  ttrclselem2  9708  rankval3b  9811  fseqenlem2  10031  dfac3  10127  dfac5  10134  dfac2b  10136  dfac8  10141  dfac9  10142  dfacacn  10147  dfac13  10148  kmlem1  10156  kmlem6  10161  kmlem13  10168  fin23lem32  10349  zornn0g  10510  fpwwe2lem10  10652  fpwwe2lem11  10653  fpwwe2lem12  10654  hargch  10685  alephgch  10686  nqpr  11026  reclem2pr  11060  hashgt23el  14492  rtrclreclem4  15137  dfrtrcl2  15138  relexpindlem  15139  shftfn  15149  ramub  17108  ramcl  17124  imasaddfnlem  17617  imasvscafn  17626  mrieqv2d  17730  mreexexd  17739  invfun  17856  joinfval  18462  meetfval  18476  mreclatBAD  18654  letsr  18684  efgval  19847  efgi  19849  efgi2  19855  gsumval3lem2  20036  gsumzaddlem  20051  pgpfac1lem5  20211  ringurd  20327  zrinitorngc  20807  zrtermorngc  20808  zrtermoringc  20840  islbs3  21345  lbsextlem4  21351  rspsn0  21438  ssdifidl  21551  cssmre  21909  obslbs  21946  mplsubglem  22216  mpllsslem  22217  tgcl  23197  indistopon  23229  ppttop  23235  epttop  23237  mretopd  23320  toponmre  23321  neissex  23355  neiptoptop  23359  lmfun  23609  2ndcdisj  23685  1stccnp  23691  kgentopon  23767  dfac14  23847  ptcnp  23851  uptx  23854  ptrescn  23868  qtoptop2  23928  filconn  24112  filssufilg  24140  rnelfmlem  24181  alexsubALTlem2  24277  cnextfun  24293  utoptop  24463  prdsxmslem2  24758  vitalilem3  25841  mbfposr  25883  mbfinf  25896  i1fd  25912  itg1climres  25945  perfdvf  26133  taylf  26600  addbdaylem  28285  noseqrdgfn  28574  n0cut  28602  mpteleeOLD  29355  upgr1eopALT  29577  upgrspanop  29760  umgrspanop  29761  usgrspanop  29762  cplgrop  29900  umgr2v2enb1  29989  clwwlknon1loop  30571  loop1cycl  30626  wlkl0  30850  ex-natded9.26  30902  ex-natded9.26-2  30903  aevdemo  30943  nmcexi  32510  iuneq12daf  33033  iinabrex  33045  abfmpeld  33130  abfmpel  33131  ssmxidl  33880  exsslsb  34110  zarclssn  34386  bnj1143  35302  bnj1379  35342  bnj149  35387  rankval4b  35610  r1omhfb  35625  fineqvac  35645  r1omhfbregs  35666  kardval  35681  gblacfnacd  35702  vonf1wev  35708  vonf1owevOLD  35710  wevgblacfn  35711  satffunlem1lem1  35984  satffunlem2lem1  35986  prv0  36012  mclsssvlem  36144  ssmclslem  36147  mclsax  36151  mclsind  36152  dfon2lem6  36368  dfon2lem8  36370  dfon2lem9  36371  dfon2  36372  trer  36938  finminlem  36940  neibastop1  36981  neibastop3  36984  weiunfr  37089  axuntco  37101  regsfromunir1  37162  mh-regprimbi  37167  unbdqndv1  37208  knoppndv  37234  bj-ssbid1ALT  37398  bj-eqs  37409  bj-sb  37423  bj-substw  37461  bj-spcimdv  37641  bj-spcimdvv  37642  bj-csbprc  37656  bj-gabss  37682  bj-elgab  37686  curryset  37693  currysetlem3  37696  bj-cleq  37709  exellimddv  38102  finorwe  38139  wl-motae  38281  wl-cbvalsbi  38312  fin2so  38364  poimirlem17  38389  mblfinlem3  38411  ismblfin  38413  itg2addnc  38426  findcard4  38466  upixp  38482  mpobi123f  38913  mptbi12f  38917  preuniqval  39247  trcoss  39323  eldisjsim5  39690  prter1  39755  axc11n-16  39814  ax12eq  39817  ax12el  39818  sticksstones22  43037  sbtd  43082  sn-axprlem3  43091  sn-exelALT  43092  ismrcd1  43546  ttac  43880  fnwe2  43897  aomclem6  43903  dfac11  43906  dfac21  43910  hbtlem2  43968  oaun3lem1  44218  cllem0  44409  clss2lem  44454  mptrcllem  44456  iunrelexpmin1  44551  iunrelexpmin2  44555  iunrelexpuztr  44562  dftrcl3  44563  brtrclfv2  44570  dfrtrcl3  44576  psshepw  44631  frege91  44797  frege97  44803  frege109  44815  frege130  44836  grumnudlem  45112  ismnushort  45128  axc11next  45233  pm13.192  45237  pm14.24  45259  gen11  45442  trsspwALT2  45644  snssiALT  45653  sstrALT2  45660  en3lpVD  45670  sspwimp  45743  sspwimpcf  45745  sspwimpALT  45750  ax6e2ndeqALT  45756  ssmapsn  46049  infnsuprnmpt  46082  uzinico  46392  icccncfext  46718  itgsinexplem1  46785  sge0resplit  47237  hspdifhsp  47447  smflimsuplem7  47657  dfatcolem  48146  iccpartdisj  48340  sbcpr  48424  eufsnlem  49772  iscnrm3lem2  49864  functhincfun  50378  termcarweu  50457  setrec2fun  50621  elsetrecslem  50628  setrecsss  50630  setrecsres  50631  0setrec  50633  pgindnf  50645