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

Theorem 2albidv 1848
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 1846 . 2 (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
32albidv 1846 1 (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  dff13  6472  qliftfun  7784  seqf1o  12790  fi1uzind  13226  brfi1indALT  13229  fi1uzindOLD  13232  brfi1indALTOLD  13235  trclfvcotr  13692  dchrelbas3  24880  isch2  27950  mclsssvlem  31202  mclsval  31203  mclsax  31209  mclsind  31210  trer  31987  mbfresfi  33123  isass  33312  lpolsetN  36286  islpolN  36287  ismrc  36779  2sbc6g  38133
  Copyright terms: Public domain W3C validator