Theorem alrimiv 1960

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2246 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  2162  cbv3v2  2280  nexmo  2571  moimdv  2576  mobidv  2579  eubidv  2616  euequ  2627  eqrdv  2763  abbidv  2831  elex22  3481  pm13.183  3627  moeq3  3677  sbc2or  3755  sbcthdv  3762  csbied  3890  ssrdv  3944  eq0rdv  4372  rabeqsnd  4637  rabsn  4689  dfnfc2  4896  intab  4945  iuneq12df  4985  elALT2  5342  reusv2lem1  5371  reusv2lem2  5372  axprlem3OLD  5402  sbcop1  5472  euotd  5498  ssrelrel  5784  relimasn  6089  asymref2  6119  dfpo2  6301  iotaval2  6511  iota5  6523  iotabidv  6524  funmo  6556  funco  6580  funun  6586  fununfun  6588  fununi  6615  nfunsn  6924  fvn0ssdmfun  7073  f1oresrab  7127  0mpo0  7502  funoprabg  7540  tfisi  7861  limom  7884  funcnvuni  7935  1stconst  8101  2ndconst  8102  frxp  8128  fnwelem  8133  frxp2  8146  frxp3  8153  frrlem9  8297  seqomlem2  8444  iserd  8727  fsetdmprc0  8858  ssfi  9164  findcard3  9250  frfi  9252  fiint  9293  dffi2  9390  hartogslem1  9511  wdomd  9550  ixpiunwdom  9559  ttrclss  9696  ttrclselem2  9702  rankval3b  9805  fseqenlem2  10025  dfac3  10121  dfac5  10128  dfac2b  10130  dfac8  10135  dfac9  10136  dfacacn  10141  dfac13  10142  kmlem1  10150  kmlem6  10155  kmlem13  10162  fin23lem32  10343  zornn0g  10504  fpwwe2lem10  10644  fpwwe2lem11  10645  fpwwe2lem12  10646  hargch  10677  alephgch  10678  nqpr  11018  reclem2pr  11052  hashgt23el  14483  rtrclreclem4  15126  dfrtrcl2  15127  relexpindlem  15128  shftfn  15138  ramub  17099  ramcl  17115  imasaddfnlem  17608  imasvscafn  17617  mrieqv2d  17721  mreexexd  17730  invfun  17847  joinfval  18453  meetfval  18467  mreclatBAD  18645  letsr  18675  efgval  19835  efgi  19837  efgi2  19843  gsumval3lem2  20024  gsumzaddlem  20039  pgpfac1lem5  20199  ringurd  20315  zrinitorngc  20795  zrtermorngc  20796  zrtermoringc  20828  islbs3  21333  lbsextlem4  21339  rspsn0  21426  ssdifidl  21539  cssmre  21897  obslbs  21934  mplsubglem  22202  mpllsslem  22203  tgcl  23180  indistopon  23212  ppttop  23218  epttop  23220  mretopd  23303  toponmre  23304  neissex  23338  neiptoptop  23342  lmfun  23592  2ndcdisj  23668  1stccnp  23674  kgentopon  23750  dfac14  23830  ptcnp  23834  uptx  23837  ptrescn  23851  qtoptop2  23911  filconn  24095  filssufilg  24123  rnelfmlem  24164  alexsubALTlem2  24260  cnextfun  24276  utoptop  24446  prdsxmslem2  24741  vitalilem3  25824  mbfposr  25866  mbfinf  25879  i1fd  25895  itg1climres  25928  perfdvf  26117  taylf  26579  addbdaylem  28265  noseqrdgfn  28554  n0cut  28582  mpteleeOLD  29304  upgr1eopALT  29526  upgrspanop  29709  umgrspanop  29710  usgrspanop  29711  cplgrop  29849  umgr2v2enb1  29938  clwwlknon1loop  30520  loop1cycl  30575  wlkl0  30793  ex-natded9.26  30845  ex-natded9.26-2  30846  aevdemo  30886  nmcexi  32453  iuneq12daf  32976  iinabrex  32989  abfmpeld  33074  abfmpel  33075  ssmxidl  33825  exsslsb  34055  zarclssn  34331  bnj1143  35247  bnj1379  35287  bnj149  35332  rankval4b  35555  r1omhfb  35570  fineqvac  35590  r1omhfbregs  35611  kardval  35626  gblacfnacd  35647  vonf1wev  35653  vonf1owevOLD  35655  wevgblacfn  35656  satffunlem1lem1  35935  satffunlem2lem1  35937  prv0  35963  mclsssvlem  36095  ssmclslem  36098  mclsax  36102  mclsind  36103  dfon2lem6  36319  dfon2lem8  36321  dfon2lem9  36322  dfon2  36323  trer  36888  finminlem  36890  neibastop1  36931  neibastop3  36934  weiunfr  37039  axuntco  37051  regsfromunir1  37112  mh-regprimbi  37117  unbdqndv1  37158  knoppndv  37184  bj-ssbid1ALT  37348  bj-eqs  37359  bj-sb  37373  bj-substw  37411  bj-spcimdv  37591  bj-spcimdvv  37592  bj-csbprc  37606  bj-gabss  37632  bj-elgab  37636  curryset  37643  currysetlem3  37646  bj-cleq  37659  exellimddv  38052  finorwe  38089  wl-motae  38231  wl-cbvalsbi  38262  fin2so  38319  poimirlem17  38349  mblfinlem3  38371  ismblfin  38373  itg2addnc  38386  findcard4  38426  upixp  38442  mpobi123f  38873  mptbi12f  38877  preuniqval  39207  trcoss  39283  eldisjsim5  39650  prter1  39715  axc11n-16  39774  ax12eq  39777  ax12el  39778  sticksstones22  42997  sbtd  43042  sn-axprlem3  43051  sn-exelALT  43052  ismrcd1  43506  ttac  43840  fnwe2  43857  aomclem6  43863  dfac11  43866  dfac21  43870  hbtlem2  43928  oaun3lem1  44178  cllem0  44369  clss2lem  44414  mptrcllem  44416  iunrelexpmin1  44511  iunrelexpmin2  44515  iunrelexpuztr  44522  dftrcl3  44523  brtrclfv2  44530  dfrtrcl3  44536  psshepw  44591  frege91  44757  frege97  44763  frege109  44775  frege130  44796  grumnudlem  45072  ismnushort  45088  axc11next  45193  pm13.192  45197  pm14.24  45219  gen11  45402  trsspwALT2  45604  snssiALT  45613  sstrALT2  45620  en3lpVD  45630  sspwimp  45703  sspwimpcf  45705  sspwimpALT  45710  ax6e2ndeqALT  45716  ssmapsn  46009  infnsuprnmpt  46042  uzinico  46352  icccncfext  46678  itgsinexplem1  46745  sge0resplit  47197  hspdifhsp  47407  smflimsuplem7  47617  dfatcolem  48069  iccpartdisj  48263  sbcpr  48347  eufsnlem  49695  iscnrm3lem2  49789  functhincfun  50303  termcarweu  50382  setrec2fun  50546  elsetrecslem  50553  setrecsss  50555  setrecsres  50556  0setrec  50558  pgindnf  50570