Theorem 2albidv 1951

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  dff13  7256  xpord2indlem  8146  xpord3inddlem  8153  qliftfun  8803  seqf1o  14082  fi1uzind  14547  brfi1indALT  14550  trclfvcotr  15049  dchrelbas3  27382  isch2  31545  isacycgr1  35596  mclsssvlem  36012  mclsval  36013  mclsax  36019  mclsind  36020  trer  36775  mbfresfi  38265  isass  38445  relcnveq2  38928  elrelscnveq2  39228  elsymrels3  39237  elsymrels5  39239  eltrrels3  39263  eleqvrels3  39276  lpolsetN  42206  islpolN  42207  ismrc  43384  2sbc6g  45077  fun2dmnopgexmpl  47970  joindm2  49695  meetdm2  49697