Theorem 2albidv 1925

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 1922	. 2 ⊢ (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
3	2	albidv 1922	1 ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  dff13  7200  xpord2indlem  8089  xpord3inddlem  8096  qliftfun  8741  seqf1o  13968  fi1uzind  14432  brfi1indALT  14435  trclfvcotr  14934  dchrelbas3  27207  isch2  31279  isacycgr1  35319  mclsssvlem  35735  mclsval  35736  mclsax  35742  mclsind  35743  trer  36489  mbfresfi  37836  isass  38016  relcnveq2  38499  elrelscnveq2  38799  elsymrels3  38808  elsymrels5  38810  eltrrels3  38834  eleqvrels3  38847  lpolsetN  41777  islpolN  41778  ismrc  42980  2sbc6g  44693  fun2dmnopgexmpl  47567  joindm2  49250  meetdm2  49252