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  7246  xpord2indlem  8142  xpord3inddlem  8149  qliftfun  8801  seqf1o  14154  fi1uzind  14619  brfi1indALT  14622  trclfvcotr  15129  dchrelbas3  27528  isacycgr1  30685  isch2  31758  mclsssvlem  36248  mclsval  36249  mclsax  36255  mclsind  36256  trer  37026  mbfresfi  38504  isass  38700  relcnveq2  39181  elrelscnveq2  39481  elsymrels3  39490  elsymrels5  39492  eltrrels3  39516  eleqvrels3  39529  lpolsetN  42459  islpolN  42460  ismrc  43650  2sbc6g  45343  fun2dmnopgexmpl  48276  joindm2  49998  meetdm2  50000