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

Theorem 2albidv 1915
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 1912 . 2 (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
32albidv 1912 1 (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  dff13  7004  qliftfun  8372  seqf1o  13401  fi1uzind  13845  brfi1indALT  13848  trclfvcotr  14359  dchrelbas3  25742  isch2  28928  isacycgr1  32291  mclsssvlem  32707  mclsval  32708  mclsax  32714  mclsind  32715  trer  33562  mbfresfi  34820  isass  35007  relcnveq2  35463  elrelscnveq2  35615  elsymrels3  35672  elsymrels5  35674  eltrrels3  35698  eleqvrels3  35710  lpolsetN  38500  islpolN  38501  ismrc  39178  2sbc6g  40627  fun2dmnopgexmpl  43364
  Copyright terms: Public domain W3C validator