Theorem 2albidv 1924

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  dff13  7188  xpord2indlem  8077  xpord3inddlem  8084  qliftfun  8726  seqf1o  13950  fi1uzind  14414  brfi1indALT  14417  trclfvcotr  14916  dchrelbas3  27176  isch2  31203  isacycgr1  35190  mclsssvlem  35606  mclsval  35607  mclsax  35613  mclsind  35614  trer  36360  mbfresfi  37705  isass  37885  relcnveq2  38360  elrelscnveq2  38640  elsymrels3  38649  elsymrels5  38651  eltrrels3  38675  eleqvrels3  38688  lpolsetN  41580  islpolN  41581  ismrc  42793  2sbc6g  44507  fun2dmnopgexmpl  47383  joindm2  49067  meetdm2  49069