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

Theorem 2albidv 1838
 Description: Formula-building rule for two universal quantifiers (deduction rule). (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 1836 . 2 (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
32albidv 1836 1 (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196 This theorem is referenced by:  dff13  6416  qliftfun  7719  seqf1o  12704  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  trclfvcotr  13598  dchrelbas3  24763  isch2  27464  mclsssvlem  30713  mclsval  30714  mclsax  30720  mclsind  30721  trer  31480  mbfresfi  32626  isass  32815  lpolsetN  35789  islpolN  35790  ismrc  36282  2sbc6g  37638
 Copyright terms: Public domain W3C validator