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  7211  xpord2indlem  8103  xpord3inddlem  8110  qliftfun  8752  seqf1o  13984  fi1uzind  14448  brfi1indALT  14451  trclfvcotr  14951  dchrelbas3  27182  isch2  31202  isacycgr1  35126  mclsssvlem  35542  mclsval  35543  mclsax  35549  mclsind  35550  trer  36297  mbfresfi  37653  isass  37833  relcnveq2  38304  elrelscnveq2  38477  elsymrels3  38538  elsymrels5  38540  eltrrels3  38564  eleqvrels3  38577  lpolsetN  41469  islpolN  41470  ismrc  42682  2sbc6g  44397  fun2dmnopgexmpl  47278  joindm2  48949  meetdm2  48951