Theorem alrimiv 1927

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  alrimivv  1928  cbvalivw  2006  aevlem0  2054  aev  2057  aev2  2058  stdpc4  2068  sbimdv  2078  sbbidv  2079  elequ2g  2124  cbv3v2  2241  nexmo  2541  moimdv  2546  mobidv  2549  eubidv  2586  euequ  2597  eqrdv  2735  abbidv  2808  raleqbidvvOLD  3335  elex2OLD  3505  elex22  3506  pm13.183  3666  moeq3  3718  sbc2or  3797  sbcthdv  3804  csbied  3935  ssrdv  3989  abssdvOLD  4069  eq0rdv  4407  disj  4450  rabeqsnd  4669  rabsn  4721  dfnfc2  4929  intab  4978  intprg  4981  iuneq12df  5018  dfiin2g  5032  mpteq12dvaOLD  5232  abexd  5325  elALT2  5369  reusv2lem1  5398  reusv2lem2  5399  axprlem3OLD  5428  sbcop1  5493  euotd  5518  ssrelrel  5806  asymref2  6137  dfpo2  6316  iotaval2  6529  iotavalOLD  6535  iota5  6544  iotabidv  6545  funmo  6581  funmoOLD  6582  funco  6606  funun  6612  fununfun  6614  fununi  6641  nfunsn  6948  fvn0ssdmfun  7094  f1oresrab  7147  0mpo0  7516  funoprabg  7554  tfisi  7880  limom  7903  funcnvuni  7954  1stconst  8125  2ndconst  8126  frxp  8151  fnwelem  8156  frxp2  8169  frxp3  8176  frrlem9  8319  seqomlem2  8491  iserd  8771  fsetdmprc0  8895  ssfi  9213  findcard3  9318  findcard3OLD  9319  frfi  9321  fiint  9366  fiintOLD  9367  dffi2  9463  hartogslem1  9582  wdomd  9621  ixpiunwdom  9630  ttrclss  9760  ttrclselem2  9766  rankval3b  9866  fseqenlem2  10065  dfac3  10161  dfac5  10169  dfac2b  10171  dfac8  10176  dfac9  10177  dfacacn  10182  dfac13  10183  kmlem1  10191  kmlem6  10196  kmlem13  10203  fin23lem32  10384  axdc2lem  10488  zornn0g  10545  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  hargch  10713  alephgch  10714  nqpr  11054  reclem2pr  11088  hashgt23el  14463  cshwsexaOLD  14863  rtrclreclem4  15100  dfrtrcl2  15101  relexpindlem  15102  shftfn  15112  ramub  17051  ramcl  17067  imasaddfnlem  17573  imasvscafn  17582  mrieqv2d  17682  mreexexd  17691  invfun  17808  joinfval  18418  meetfval  18432  mreclatBAD  18608  letsr  18638  efgval  19735  efgi  19737  efgi2  19743  gsumval3lem2  19924  gsumzaddlem  19939  pgpfac1lem5  20099  ringurd  20182  zrinitorngc  20642  zrtermorngc  20643  zrtermoringc  20675  islbs3  21157  lbsextlem4  21163  cssmre  21711  obslbs  21750  mplsubglem  22019  mpllsslem  22020  tgcl  22976  indistopon  23008  ppttop  23014  epttop  23016  mretopd  23100  toponmre  23101  neissex  23135  neiptoptop  23139  lmfun  23389  2ndcdisj  23464  1stccnp  23470  kgentopon  23546  dfac14  23626  ptcnp  23630  uptx  23633  ptrescn  23647  qtoptop2  23707  filconn  23891  filssufilg  23919  rnelfmlem  23960  alexsubALTlem2  24056  cnextfun  24072  utoptop  24243  prdsxmslem2  24542  vitalilem3  25645  mbfposr  25687  mbfinf  25700  i1fd  25716  itg1climres  25749  perfdvf  25938  taylf  26402  addsbdaylem  28049  noseqrdgfn  28312  n0scut  28338  mptelee  28910  upgr1eopALT  29134  upgrspanop  29314  umgrspanop  29315  usgrspanop  29316  cplgrop  29454  umgr2v2enb1  29544  clwwlknon1loop  30117  wlkl0  30386  ex-natded9.26  30438  ex-natded9.26-2  30439  aevdemo  30479  nmcexi  32045  iuneq12daf  32569  iinabrex  32582  abfmpeld  32664  abfmpel  32665  fpwrelmap  32744  ssdifidl  33485  ssmxidl  33502  exsslsb  33647  zarclssn  33872  bnj1143  34804  bnj1379  34844  bnj149  34889  fineqvac  35111  gblacfnacd  35113  wevgblacfn  35114  loop1cycl  35142  satffunlem1lem1  35407  satffunlem2lem1  35409  prv0  35435  mclsssvlem  35567  ssmclslem  35570  mclsax  35574  mclsind  35575  dfon2lem6  35789  dfon2lem8  35791  dfon2lem9  35792  dfon2  35793  trer  36317  finminlem  36319  neibastop1  36360  neibastop3  36363  weiunfr  36468  unbdqndv1  36509  knoppndv  36535  bj-ssbid1ALT  36666  bj-eqs  36676  bj-sb  36688  bj-substw  36723  bj-nnfbd  36727  bj-spcimdv  36896  bj-spcimdvv  36897  bj-csbprc  36911  bj-gabss  36936  bj-elgab  36940  curryset  36947  currysetlem3  36950  bj-cleq  36963  exellimddv  37346  finorwe  37383  wl-motae  37516  wl-cbvalsbi  37547  fin2so  37614  poimirlem17  37644  mblfinlem3  37666  ismblfin  37668  itg2addnc  37681  upixp  37736  mpobi123f  38169  mptbi12f  38173  trcoss  38483  prter1  38880  axc11n-16  38939  ax12eq  38942  ax12el  38943  sticksstones22  42169  sbtd  42250  sn-axprlem3  42256  sn-exelALT  42257  ismrcd1  42709  ttac  43048  fnwe2  43065  aomclem6  43071  dfac11  43074  dfac21  43078  hbtlem2  43136  oaun3lem1  43387  cllem0  43579  clss2lem  43624  mptrcllem  43626  iunrelexpmin1  43721  iunrelexpmin2  43725  iunrelexpuztr  43732  dftrcl3  43733  brtrclfv2  43740  dfrtrcl3  43746  psshepw  43801  frege91  43967  frege97  43973  frege109  43985  frege130  44006  grumnudlem  44304  ismnushort  44320  axc11next  44425  pm13.192  44429  pm14.24  44451  gen11  44636  trsspwALT2  44839  snssiALT  44848  sstrALT2  44855  en3lpVD  44865  sspwimp  44938  sspwimpcf  44940  sspwimpALT  44945  ax6e2ndeqALT  44951  ssmapsn  45221  infnsuprnmpt  45257  uzinico  45573  icccncfext  45902  itgsinexplem1  45969  sge0resplit  46421  hoidmvlelem1  46610  hspdifhsp  46631  smflimsuplem7  46841  dfatcolem  47267  iccpartdisj  47424  sbcpr  47508  eufsnlem  48750  iscnrm3lem2  48832  functhincfun  49098  setrec2fun  49211  elsetrecslem  49218  setrecsss  49220  setrecsres  49221  0setrec  49223  pgindnf  49235