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 209  ∀wal 1536

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  dff13  6991  qliftfun  8365  seqf1o  13407  fi1uzind  13851  brfi1indALT  13854  trclfvcotr  14360  dchrelbas3  25822  isch2  29006  isacycgr1  32506  mclsssvlem  32922  mclsval  32923  mclsax  32929  mclsind  32930  trer  33777  mbfresfi  35103  isass  35284  relcnveq2  35740  elrelscnveq2  35893  elsymrels3  35950  elsymrels5  35952  eltrrels3  35976  eleqvrels3  35988  lpolsetN  38778  islpolN  38779  ismrc  39642  2sbc6g  41119  fun2dmnopgexmpl  43840