Theorem 2albidv 1919

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1532

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 1906

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  dff13  7259  xpord2indlem  8146  xpord3inddlem  8153  qliftfun  8814  seqf1o  14034  fi1uzind  14484  brfi1indALT  14487  trclfvcotr  14982  dchrelbas3  27164  isch2  31026  isacycgr1  34746  mclsssvlem  35162  mclsval  35163  mclsax  35169  mclsind  35170  trer  35790  mbfresfi  37128  isass  37308  relcnveq2  37784  elrelscnveq2  37954  elsymrels3  38015  elsymrels5  38017  eltrrels3  38041  eleqvrels3  38054  lpolsetN  40944  islpolN  40945  ismrc  42093  2sbc6g  43824  fun2dmnopgexmpl  46636  joindm2  47959  meetdm2  47961