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

Step	Hyp	Ref	Expression
1		2albidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	albidv 1920	. 2 ⊢ (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
3	2	albidv 1920	1 ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒))

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  7191  xpord2indlem  8080  xpord3inddlem  8087  qliftfun  8729  seqf1o  13950  fi1uzind  14414  brfi1indALT  14417  trclfvcotr  14916  dchrelbas3  27147  isch2  31171  isacycgr1  35139  mclsssvlem  35555  mclsval  35556  mclsax  35562  mclsind  35563  trer  36310  mbfresfi  37666  isass  37846  relcnveq2  38317  elrelscnveq2  38490  elsymrels3  38551  elsymrels5  38553  eltrrels3  38577  eleqvrels3  38590  lpolsetN  41481  islpolN  41482  ismrc  42694  2sbc6g  44408  fun2dmnopgexmpl  47288  joindm2  48972  meetdm2  48974