Theorem 2albidv 2022

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

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009

This theorem depends on definitions:  df-bi 199

This theorem is referenced by:  dff13  6767  qliftfun  8097  seqf1o  13136  fi1uzind  13568  brfi1indALT  13571  trclfvcotr  14127  dchrelbas3  25376  isch2  28624  mclsssvlem  31994  mclsval  31995  mclsax  32001  mclsind  32002  trer  32838  mbfresfi  33992  isass  34180  relcnveq2  34635  elrelscnveq2  34784  elsymrels3  34841  elsymrels5  34843  eltrrels3  34867  eleqvrels3  34878  lpolsetN  37550  islpolN  37551  ismrc  38101  2sbc6g  39448