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

Theorem 2albidv 1891
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 1889 . 2 (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
32albidv 1889 1 (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  dff13  6552  qliftfun  7875  seqf1o  12882  fi1uzind  13317  brfi1indALT  13320  trclfvcotr  13794  dchrelbas3  25008  isch2  28208  mclsssvlem  31585  mclsval  31586  mclsax  31592  mclsind  31593  trer  32435  mbfresfi  33586  isass  33775  relcnveq2  34235  elrelscnveq2  34383  elsymrels3  34440  elsymrels5  34442  lpolsetN  37088  islpolN  37089  ismrc  37581  2sbc6g  38933
  Copyright terms: Public domain W3C validator