Theorem 2albidv 1956

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210

This theorem is used by:  dff13  7254  xpord2indlem  8148  xpord3inddlem  8155  qliftfun  8805  seqf1o  14109  fi1uzind  14574  brfi1indALT  14577  trclfvcotr  15084  dchrelbas3  27472  isacycgr1  30617  isch2  31690  mclsssvlem  36128  mclsval  36129  mclsax  36135  mclsind  36136  trer  36922  mbfresfi  38402  isass  38583  relcnveq2  39064  elrelscnveq2  39364  elsymrels3  39373  elsymrels5  39375  eltrrels3  39399  eleqvrels3  39412  lpolsetN  42342  islpolN  42343  ismrc  43533  2sbc6g  45226  fun2dmnopgexmpl  48159  joindm2  49881  meetdm2  49883