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 208  ∀wal 1529

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

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  dff13  7005  qliftfun  8374  seqf1o  13403  fi1uzind  13847  brfi1indALT  13850  trclfvcotr  14361  dchrelbas3  25806  isch2  28992  isacycgr1  32386  mclsssvlem  32802  mclsval  32803  mclsax  32809  mclsind  32810  trer  33657  mbfresfi  34930  isass  35116  relcnveq2  35572  elrelscnveq2  35725  elsymrels3  35782  elsymrels5  35784  eltrrels3  35808  eleqvrels3  35820  lpolsetN  38610  islpolN  38611  ismrc  39288  2sbc6g  40737  fun2dmnopgexmpl  43473