Theorem 2albidv 1918

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  dff13  7246  xpord2indlem  8127  xpord3inddlem  8134  qliftfun  8791  seqf1o  14005  fi1uzind  14454  brfi1indALT  14457  trclfvcotr  14952  dchrelbas3  27075  isch2  30900  isacycgr1  34592  mclsssvlem  35008  mclsval  35009  mclsax  35015  mclsind  35016  trer  35657  mbfresfi  36990  isass  37170  relcnveq2  37648  elrelscnveq2  37819  elsymrels3  37880  elsymrels5  37882  eltrrels3  37906  eleqvrels3  37919  lpolsetN  40809  islpolN  40810  ismrc  41894  2sbc6g  43629  fun2dmnopgexmpl  46443  joindm2  47755  meetdm2  47757