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

Theorem 2albidv 1923
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 1920 . 2 (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
32albidv 1920 1 (𝜑 → (∀𝑥𝑦𝜓 ↔ ∀𝑥𝑦𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207
This theorem is referenced by:  dff13  7275  xpord2indlem  8172  xpord3inddlem  8179  qliftfun  8842  seqf1o  14084  fi1uzind  14546  brfi1indALT  14549  trclfvcotr  15048  dchrelbas3  27282  isch2  31242  isacycgr1  35151  mclsssvlem  35567  mclsval  35568  mclsax  35574  mclsind  35575  trer  36317  mbfresfi  37673  isass  37853  relcnveq2  38324  elrelscnveq2  38494  elsymrels3  38555  elsymrels5  38557  eltrrels3  38581  eleqvrels3  38594  lpolsetN  41484  islpolN  41485  ismrc  42712  2sbc6g  44434  fun2dmnopgexmpl  47296  joindm2  48865  meetdm2  48867
  Copyright terms: Public domain W3C validator