MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alimdv Structured version   Visualization version   GIF version

Theorem alimdv 1832
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1729. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
alimdv (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem alimdv
StepHypRef Expression
1 ax-5 1827 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1735 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem is referenced by:  2alimdv  1834  ax12v2  2036  ax12vOLD  2037  ax12vOLDOLD  2038  ax13lem1  2236  axc16i  2310  ralimdv2  2944  mo2icl  3352  sstr2  3575  reuss2  3866  ssuni  4395  ssuniOLD  4396  disjss2  4556  disjss1  4559  disjiun  4573  disjss3  4582  alxfr  4804  frss  5005  ssrel  5130  ssrelOLD  5131  ssrel2  5133  ssrelrel  5143  iotaval  5779  fvn0ssdmfun  6258  dff3  6280  dfwe2  6873  ordom  6966  findcard3  8088  dffi2  8212  indcardi  8747  zorn2lem4  9204  uzindi  12643  caubnd  13946  ramtlecl  15542  psgnunilem4  17740  dfcon2  21032  wilthlem3  24596  nbcusgra  25992  disjss1f  28768  ssrelf  28805  ss2mcls  30719  mclsax  30720  wzel  31015  wzelOLD  31016  onsuct0  31610  bj-ssbim  31810  wl-ax13lem1  32466  axc11next  37629  nrhmzr  41663  setrec1lem2  42234
  Copyright terms: Public domain W3C validator