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

Theorem 2albidv 1927
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 1924 . 2 (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
32albidv 1924 1 (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206
This theorem is referenced by:  dff13  7248  xpord2indlem  8127  xpord3inddlem  8134  qliftfun  8791  seqf1o  14004  fi1uzind  14453  brfi1indALT  14456  trclfvcotr  14951  dchrelbas3  26720  isch2  30453  isacycgr1  34074  mclsssvlem  34490  mclsval  34491  mclsax  34497  mclsind  34498  trer  35138  mbfresfi  36471  isass  36651  relcnveq2  37129  elrelscnveq2  37300  elsymrels3  37361  elsymrels5  37363  eltrrels3  37387  eleqvrels3  37400  lpolsetN  40290  islpolN  40291  ismrc  41371  2sbc6g  43106  fun2dmnopgexmpl  45926  joindm2  47502  meetdm2  47504
  Copyright terms: Public domain W3C validator