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  7202  xpord2indlem  8091  xpord3inddlem  8098  qliftfun  8743  seqf1o  13970  fi1uzind  14434  brfi1indALT  14437  trclfvcotr  14936  dchrelbas3  27209  isch2  31302  isacycgr1  35342  mclsssvlem  35758  mclsval  35759  mclsax  35765  mclsind  35766  trer  36512  mbfresfi  37869  isass  38049  relcnveq2  38532  elrelscnveq2  38832  elsymrels3  38841  elsymrels5  38843  eltrrels3  38867  eleqvrels3  38880  lpolsetN  41810  islpolN  41811  ismrc  43010  2sbc6g  44723  fun2dmnopgexmpl  47597  joindm2  49280  meetdm2  49282