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

Theorem 2albidv 1966
Description: Formula-building rule for two universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
2albidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
2albidv (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem 2albidv
StepHypRef Expression
1 2albidv.1 . . 3 (𝜑 → (𝜓𝜒))
21albidv 1963 . 2 (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
32albidv 1963 1 (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953
This theorem depends on definitions:  df-bi 199
This theorem is referenced by:  dff13  6784  qliftfun  8115  seqf1o  13160  fi1uzind  13593  brfi1indALT  13596  trclfvcotr  14157  dchrelbas3  25415  isch2  28652  mclsssvlem  32058  mclsval  32059  mclsax  32065  mclsind  32066  trer  32899  mbfresfi  34081  isass  34269  relcnveq2  34722  elrelscnveq2  34871  elsymrels3  34928  elsymrels5  34930  eltrrels3  34954  eleqvrels3  34965  lpolsetN  37636  islpolN  37637  ismrc  38224  2sbc6g  39571
  Copyright terms: Public domain W3C validator