Theorem 2albidv 1958

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

This proof depends on definitions:  df-bi 210

This theorem is used by:  dff13  7278  xpord2indlem  8188  xpord3inddlem  8195  qliftfun  8848  seqf1o  14210  fi1uzind  14676  brfi1indALT  14679  trclfvcotr  15188  dchrelbas3  27592  isacycgr1  30779  isch2  31852  mclsssvlem  36493  mclsval  36494  mclsax  36500  mclsind  36501  trer  37281  mbfresfi  38775  isass  38971  relcnveq2  39452  elrelscnveq2  39752  elsymrels3  39761  elsymrels5  39763  eltrrels3  39787  eleqvrels3  39800  lpolsetN  42730  islpolN  42731  ismrc  43903  iunrelexpuztr  44909  2sbc6g  45589  fun2dmnopgexmpl  48557  joindm2  50285  meetdm2  50287