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

Theorem 2albidv 2022
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 2019 . 2 (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
32albidv 2019 1 (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1654
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009
This theorem depends on definitions:  df-bi 199
This theorem is referenced by:  dff13  6767  qliftfun  8097  seqf1o  13136  fi1uzind  13568  brfi1indALT  13571  trclfvcotr  14127  dchrelbas3  25376  isch2  28624  mclsssvlem  31994  mclsval  31995  mclsax  32001  mclsind  32002  trer  32838  mbfresfi  33992  isass  34180  relcnveq2  34635  elrelscnveq2  34784  elsymrels3  34841  elsymrels5  34843  eltrrels3  34867  eleqvrels3  34878  lpolsetN  37550  islpolN  37551  ismrc  38101  2sbc6g  39448
  Copyright terms: Public domain W3C validator