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  3935  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  6300  iotaval2  6510  iota5  6522  iotabidv  6523  funmo  6555  funco  6581  funun  6587  fununfun  6589  fununi  6616  nfunsn  6925  fvn0ssdmfun  7075  f1oresrab  7129  0mpo0  7504  funoprabg  7542  tfisi  7871  limom  7894  funcnvuni  7945  1stconst  8112  2ndconst  8113  frxp  8139  fnwelem  8144  fnwe2  8150  frxp2  8162  frxp3  8169  frrlem9  8313  seqomlem2  8462  iserd  8745  fsetdmprc0  8878  ssfi  9189  findcard3  9275  frfi  9277  fiint  9319  dffi2  9416  hartogslem1  9537  wdomd  9576  ixpiunwdom  9585  ttrclss  9722  ttrclselem2  9728  rankval3b  9837  rankval4b  9881  hfpw  9927  setrec2fun  9974  fseqenlem2  10105  dfac3  10201  dfac5  10208  dfac2b  10210  dfac8  10215  dfac9  10216  dfacacn  10221  dfac13  10222  kmlem1  10230  kmlem6  10235  kmlem13  10242  fin23lem32  10423  zornn0g  10584  fpwwe2lem10  10726  fpwwe2lem11  10727  fpwwe2lem12  10728  hargch  10759  alephgch  10760  nqpr  11100  reclem2pr  11134  hashgt23el  14570  rtrclreclem4  15215  dfrtrcl2  15216  relexpindlem  15217  shftfn  15227  ramub  17192  ramcl  17208  imasaddfnlem  17701  imasvscafn  17710  mrieqv2d  17814  mreexexd  17823  invfun  17940  joinfval  18546  meetfval  18560  mreclatBAD  18738  letsr  18768  efgval  19932  efgi  19934  efgi2  19940  gsumval3lem2  20121  gsumzaddlem  20136  pgpfac1lem5  20296  ringurd  20412  zrinitorngc  20895  zrtermorngc  20896  zrtermoringc  20928  islbs3  21434  lbsextlem4  21440  rspsn0  21527  ssdifidl  21642  cssmre  22000  obslbs  22037  mplsubglem  22307  mpllsslem  22308  tgcl  23288  indistopon  23320  ppttop  23326  epttop  23328  mretopd  23411  toponmre  23412  neissex  23446  neiptoptop  23450  lmfun  23700  2ndcdisj  23776  1stccnp  23782  kgentopon  23858  dfac14  23938  ptcnp  23942  uptx  23945  ptrescn  23959  qtoptop2  24019  filconn  24203  filssufilg  24231  rnelfmlem  24272  alexsubALTlem2  24368  cnextfun  24384  utoptop  24554  prdsxmslem2  24849  vitalilem3  25932  mbfposr  25974  mbfinf  25987  i1fd  26003  itg1climres  26036  perfdvf  26224  taylf  26689  addbdaylem  28404  noseqrdgfn  28693  n0cut  28721  mpteleeOLD  29474  upgr1eopALT  29696  upgrspanop  29879  umgrspanop  29880  usgrspanop  29881  cplgrop  30019  umgr2v2enb1  30108  clwwlknon1loop  30690  loop1cycl  30745  wlkl0  30969  ex-natded9.26  31021  ex-natded9.26-2  31022  aevdemo  31062  nmcexi  32629  iuneq12daf  33152  iinabrex  33164  abfmpeld  33249  abfmpel  33250  ssmxidl  34000  exsslsb  34230  zarclssn  34506  bnj1143  35421  bnj1379  35461  bnj149  35506  r1omhfb  35739  fineqvac  35785  r1omhfbregs  35806  kardval  35821  gblacfnacd  35882  vonf1wev  35888  vonf1owevOLD  35890  wevgblacfn  35891  vonf1onprcf1ac  35895  onprcf1acwevdlem2  35897  satffunlem1lem1  36168  satffunlem2lem1  36170  prv0  36196  mclsssvlem  36328  ssmclslem  36331  mclsax  36335  mclsind  36336  dfon2lem6  36551  dfon2lem8  36553  dfon2lem9  36554  dfon2  36555  trer  37105  finminlem  37107  neibastop1  37148  neibastop3  37151  weiunfr  37256  axuntco  37268  regsfromunir1  37329  mh-regprimbi  37334  unbdqndv1  37375  knoppndv  37401  bj-ssbid1ALT  37565  bj-eqs  37576  bj-sb  37590  bj-substw  37628  bj-spcimdv  37808  bj-spcimdvv  37809  bj-csbprc  37823  bj-gabss  37849  bj-elgab  37853  curryset  37860  currysetlem3  37863  bj-cleq  37876  exellimddv  38270  finorwe  38307  wl-motae  38449  wl-cbvalsbi  38480  fin2so  38532  poimirlem17  38557  mblfinlem3  38579  ismblfin  38581  itg2addnc  38594  findcard4  38634  varprop  38644  negprop  38645  impprop  38646  upixp  38665  mpobi123f  39096  mptbi12f  39100  preuniqval  39430  trcoss  39506  eldisjsim5  39873  prter1  39938  axc11n-16  39997  ax12eq  40000  ax12el  40001  sticksstones22  43220  sbtd  43265  sn-axprlem3  43274  sn-exelALT  43275  ismrcd1  43710  ttac  44044  aomclem6  44062  dfac11  44065  dfac21  44069  hbtlem2  44127  oaun3lem1  44377  cllem0  44568  clss2lem  44612  mptrcllem  44614  iunrelexpmin1  44709  iunrelexpmin2  44713  iunrelexpuztr  44720  dftrcl3  44721  brtrclfv2  44728  dfrtrcl3  44734  psshepw  44789  frege91  44955  frege97  44961  frege109  44973  frege130  44994  grumnudlem  45270  ismnushort  45286  axc11next  45391  pm13.192  45395  pm14.24  45417  gen11  45600  trsspwALT2  45802  snssiALT  45811  sstrALT2  45818  en3lpVD  45828  sspwimp  45901  sspwimpcf  45903  sspwimpALT  45908  ax6e2ndeqALT  45914  ssmapsn  46230  infnsuprnmpt  46263  uzinico  46572  icccncfext  46898  itgsinexplem1  46965  sge0resplit  47417  hspdifhsp  47627  smflimsuplem7  47837  dfatcolem  48326  iccpartdisj  48520  sbcpr  48604  eufsnlem  49952  iscnrm3lem2  50044  functhincfun  50558  termcarweu  50637  elsetrecslem  50793  setrecsss  50795  setrecsres  50796  0setrec  50798  pgindnf  50810