Theorem 2albidv 1920

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  dff13  7007  qliftfun  8376  seqf1o  13405  fi1uzind  13849  brfi1indALT  13852  trclfvcotr  14363  dchrelbas3  25808  isch2  28994  isacycgr1  32388  mclsssvlem  32804  mclsval  32805  mclsax  32811  mclsind  32812  trer  33659  mbfresfi  34932  isass  35118  relcnveq2  35574  elrelscnveq2  35727  elsymrels3  35784  elsymrels5  35786  eltrrels3  35810  eleqvrels3  35822  lpolsetN  38612  islpolN  38613  ismrc  39291  2sbc6g  40740  fun2dmnopgexmpl  43477