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

Theorem 2albidv 1924
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 1921 . 2 (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
32albidv 1921 1 (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210
This theorem is referenced by:  dff13  6996  qliftfun  8369  seqf1o  13407  fi1uzind  13851  brfi1indALT  13854  trclfvcotr  14360  dchrelbas3  25820  isch2  29004  isacycgr1  32467  mclsssvlem  32883  mclsval  32884  mclsax  32890  mclsind  32891  trer  33738  mbfresfi  35061  isass  35242  relcnveq2  35698  elrelscnveq2  35851  elsymrels3  35908  elsymrels5  35910  eltrrels3  35934  eleqvrels3  35946  lpolsetN  38736  islpolN  38737  ismrc  39572  2sbc6g  41053  fun2dmnopgexmpl  43779
  Copyright terms: Public domain W3C validator