Theorem 2albidv 1925

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540

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 1912

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  dff13  7212  xpord2indlem  8101  xpord3inddlem  8108  qliftfun  8753  seqf1o  13980  fi1uzind  14444  brfi1indALT  14447  trclfvcotr  14946  dchrelbas3  27222  isch2  31317  isacycgr1  35368  mclsssvlem  35784  mclsval  35785  mclsax  35791  mclsind  35792  trer  36538  mbfresfi  37946  isass  38126  relcnveq2  38609  elrelscnveq2  38909  elsymrels3  38918  elsymrels5  38920  eltrrels3  38944  eleqvrels3  38957  lpolsetN  41887  islpolN  41888  ismrc  43087  2sbc6g  44800  fun2dmnopgexmpl  47673  joindm2  49356  meetdm2  49358