Theorem alrimivv 1960

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2243 and 19.21v 1971. (Contributed by NM, 31-Jul-1995.)

Hypothesis

Ref	Expression
alrimivv.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alrimivv	⊢ (𝜑 → ∀𝑥∀𝑦𝜓)

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥, 𝑦)

Proof of Theorem alrimivv

Step	Hyp	Ref	Expression
1		alrimivv.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	alrimiv 1959	. 2 ⊢ (𝜑 → ∀𝑦𝜓)
3	2	alrimiv 1959	1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)

This proof depends on syntax axioms:   → wi 4  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1827  ax-4 1841  ax-5 1942

This theorem is used by:  2ax5  1969  2mo  2673  euind  3681  sbnfc2  4396  uniintsn  4944  eusvnf  5353  copsex2dv  5465  ssopab2dv  5525  ssrel  5758  relssdv  5763  eqrelrdv  5767  eqbrrdv  5768  eqrelrdv2  5770  ssrelrel  5771  iss  6026  iresn0n0  6045  ordelord  6384  suctr  6451  funssres  6584  funun  6586  fununi  6615  fsn  7136  ovg  7585  wemoiso  7985  wemoiso2  7986  oprabexd  7987  frrlem9  8312  omeu  8593  qliftfund  8824  eroveu  8833  fpwwe2lem10  10725  addsrmo  11158  mulsrmo  11159  seqf1o  14186  fi1uzind  14652  brfi1indALT  14655  summo  15883  prodmo  16103  pceu  17024  invfun  17939  initoeu2lem2  18190  psss  18754  psgneu  19720  gsumval3eu  20118  hausflimi  24299  vitalilem3  25931  plyexmo  26636  nosupprefixmo  28057  noinfprefixmo  28058  nosupno  28060  noinfno  28075  bdayons  28662  tglineintmo  29110  frgr3vlem1  30874  3vfriswmgrlem  30878  frgr2wwlk1  30930  pjhthmo  31904  chscl  32243  bnj1379  35460  bnj580  35543  bnj1321  35657  acycgr1v  35914  cvmlift2lem12  36079  satffunlem1lem1  36167  satffunlem2lem1  36169  mclsssvlem  36327  mclsax  36334  mclsind  36335  lineintmo  36922  trer  37104  mbfresfi  38585  unirep  38649  iss2  39277  prter1  39937  islpoldN  42542  ismrcd2  43710  ismrc  43712  tfsconcatb0  44346  mnutrd  45264  truniALT  45524  gen12  45601  sspwtrALT  45804  sspwtrALT2  45805  suctrALT  45808  suctrALT2  45819  trintALT  45863  suctrALTcf  45904  suctrALT3  45906  rlimdmafv  48247  rlimdmafv2  48328  opabresex0d  48355  spr0nelg  48558  sprsymrelfvlem  48572  mofsn  49954  thincmo  50536  functhincfun  50557