Theorem alrimiv 1930

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem is referenced by:  alrimivv  1931  cbvalivw  2010  aevlem0  2057  aev  2060  aev2  2061  stdpc4  2071  sbimdv  2081  sbbidv  2082  elequ2g  2122  cbv3v2  2234  nexmo  2535  moimdv  2540  mobidv  2543  eubidv  2580  euequ  2591  eqrdv  2730  abbidv  2801  raleqbidvvOLD  3330  elex2OLD  3495  elex22  3496  ceqsexvOLD  3526  pm13.183  3655  moeq3  3707  sbc2or  3785  sbcthdv  3792  sbcimdvOLD  3851  csbied  3930  ssrdv  3987  ss2abdvOLD  4061  abssdvOLD  4065  eq0rdv  4403  disj  4446  rabeqsnd  4670  rabsn  4724  dfnfc2  4932  intab  4981  intprg  4984  iuneq12df  5022  dfiin2g  5034  mpteq12dvaOLD  5237  elALT2  5366  reusv2lem1  5395  reusv2lem2  5396  axprlem3  5422  sbcop1  5487  euotd  5512  ssrelrel  5794  asymref2  6115  dfpo2  6292  iotaval2  6508  iotavalOLD  6514  iota5  6523  iotabidv  6524  funmo  6560  funmoOLD  6561  funco  6585  funun  6591  fununfun  6593  fununi  6620  nfunsn  6930  fvn0ssdmfun  7073  f1oresrab  7121  0mpo0  7488  funoprabg  7525  tfisi  7844  limom  7867  funcnvuni  7918  1stconst  8082  2ndconst  8083  frxp  8108  fnwelem  8113  frxp2  8126  frxp3  8133  frrlem9  8275  seqomlem2  8447  iserd  8725  fsetdmprc0  8845  ssfi  9169  findcard3  9281  findcard3OLD  9282  frfi  9284  fiint  9320  dffi2  9414  hartogslem1  9533  wdomd  9572  ixpiunwdom  9581  ttrclss  9711  ttrclselem2  9717  rankval3b  9817  fseqenlem2  10016  dfac3  10112  dfac5  10119  dfac2b  10121  dfac8  10126  dfac9  10127  dfacacn  10132  dfac13  10133  kmlem1  10141  kmlem6  10146  kmlem13  10153  fin23lem32  10335  axdc2lem  10439  zornn0g  10496  fpwwe2lem10  10631  fpwwe2lem11  10632  fpwwe2lem12  10633  hargch  10664  alephgch  10665  nqpr  11005  reclem2pr  11039  hashgt23el  14380  cshwsexaOLD  14771  rtrclreclem4  15004  dfrtrcl2  15005  relexpindlem  15006  shftfn  15016  ramub  16942  ramcl  16958  imasaddfnlem  17470  imasvscafn  17479  mrieqv2d  17579  mreexexd  17588  invfun  17707  joinfval  18322  meetfval  18336  mreclatBAD  18512  letsr  18542  efgval  19579  efgi  19581  efgi2  19587  gsumval3lem2  19768  gsumzaddlem  19783  pgpfac1lem5  19943  islbs3  20760  lbsextlem4  20766  cssmre  21237  obslbs  21276  mplsubglem  21549  mpllsslem  21550  tgcl  22463  indistopon  22495  ppttop  22501  epttop  22503  mretopd  22587  toponmre  22588  neissex  22622  neiptoptop  22626  lmfun  22876  2ndcdisj  22951  1stccnp  22957  kgentopon  23033  dfac14  23113  ptcnp  23117  uptx  23120  ptrescn  23134  qtoptop2  23194  filconn  23378  filssufilg  23406  rnelfmlem  23447  alexsubALTlem2  23543  cnextfun  23559  utoptop  23730  prdsxmslem2  24029  vitalilem3  25118  mbfposr  25160  mbfinf  25173  i1fd  25189  itg1climres  25223  perfdvf  25411  taylf  25864  mptelee  28142  upgr1eopALT  28366  upgrspanop  28543  umgrspanop  28544  usgrspanop  28545  cplgrop  28683  umgr2v2enb1  28772  clwwlknon1loop  29340  wlkl0  29609  ex-natded9.26  29661  ex-natded9.26-2  29662  aevdemo  29702  nmcexi  31266  iuneq12daf  31775  iinabrex  31787  abfmpeld  31866  abfmpel  31867  fpwrelmap  31945  rngurd  32367  ssmxidl  32578  zarclssn  32841  bnj1143  33789  bnj1379  33829  bnj149  33874  fineqvac  34085  loop1cycl  34116  satffunlem1lem1  34381  satffunlem2lem1  34383  prv0  34409  mclsssvlem  34541  ssmclslem  34544  mclsax  34548  mclsind  34549  dfon2lem6  34748  dfon2lem8  34750  dfon2lem9  34751  dfon2  34752  trer  35189  finminlem  35191  neibastop1  35232  neibastop3  35235  unbdqndv1  35372  knoppndv  35398  bj-ssbid1ALT  35530  bj-eqs  35540  bj-sb  35553  bj-substw  35588  bj-nnfbd  35592  bj-spcimdv  35763  bj-spcimdvv  35764  bj-csbprc  35778  bj-gabss  35803  bj-elgab  35807  curryset  35815  currysetlem3  35818  bj-cleq  35831  exellimddv  36214  finorwe  36251  wl-motae  36372  wl-cbvalsbi  36402  fin2so  36463  poimirlem17  36493  mblfinlem3  36515  ismblfin  36517  itg2addnc  36530  upixp  36585  mpobi123f  37018  mptbi12f  37022  trcoss  37340  prter1  37737  axc11n-16  37796  ax12eq  37799  ax12el  37800  sticksstones22  40972  sbtd  41022  sn-axprlem3  41030  sn-exelALT  41031  ismrcd1  41421  ttac  41760  fnwe2  41780  aomclem6  41786  dfac11  41789  dfac21  41793  hbtlem2  41851  oaun3lem1  42109  cllem0  42302  clss2lem  42347  mptrcllem  42349  iunrelexpmin1  42444  iunrelexpmin2  42448  iunrelexpuztr  42455  dftrcl3  42456  brtrclfv2  42463  dfrtrcl3  42469  psshepw  42524  frege91  42690  frege97  42696  frege109  42708  frege130  42729  grumnudlem  43029  ismnushort  43045  axc11next  43150  pm13.192  43154  pm14.24  43176  gen11  43362  trsspwALT2  43565  snssiALT  43574  sstrALT2  43581  en3lpVD  43591  sspwimp  43664  sspwimpcf  43666  sspwimpALT  43671  ax6e2ndeqALT  43677  ssmapsn  43900  infnsuprnmpt  43940  uzinico  44259  icccncfext  44589  itgsinexplem1  44656  sge0resplit  45108  hoidmvlelem1  45297  hspdifhsp  45318  smflimsuplem7  45528  dfatcolem  45949  iccpartdisj  46091  sbcpr  46175  zrinitorngc  46851  zrtermorngc  46852  zrtermoringc  46921  eufsnlem  47460  iscnrm3lem2  47520  setrec2fun  47690  elsetrecslem  47697  setrecsss  47699  setrecsres  47700  0setrec  47702  pgindnf  47714