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

Theorem alimdv 1831
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1728. (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 1826 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2alimdh 1734 1 (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem is referenced by:  2alimdv  1833  ax12v2  2035  ax12vOLD  2036  ax12vOLDOLD  2037  ax13lem1  2235  axc16i  2309  ralimdv2  2943  mo2icl  3351  sstr2  3574  reuss2  3865  ssuni  4389  ssuniOLD  4390  disjss2  4550  disjss1  4553  disjiun  4567  disjss3  4576  alxfr  4799  frss  4995  ssrel  5120  ssrel2  5122  ssrelrel  5132  iotaval  5765  fvn0ssdmfun  6243  dff3  6265  dfwe2  6851  ordom  6944  findcard3  8066  dffi2  8190  indcardi  8725  zorn2lem4  9182  uzindi  12601  caubnd  13895  ramtlecl  15491  psgnunilem4  17689  dfcon2  20980  wilthlem3  24541  nbcusgra  25786  disjss1f  28602  ssrelf  28639  ss2mcls  30553  mclsax  30554  wzel  30849  wzelOLD  30850  onsuct0  31444  bj-ssbim  31644  wl-ax13lem1  32290  axc11next  37453  nrhmzr  41685
  Copyright terms: Public domain W3C validator