Theorem 2albidv 1927

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  dff13  7248  xpord2indlem  8127  xpord3inddlem  8134  qliftfun  8791  seqf1o  14004  fi1uzind  14453  brfi1indALT  14456  trclfvcotr  14951  dchrelbas3  26720  isch2  30453  isacycgr1  34074  mclsssvlem  34490  mclsval  34491  mclsax  34497  mclsind  34498  trer  35138  mbfresfi  36471  isass  36651  relcnveq2  37129  elrelscnveq2  37300  elsymrels3  37361  elsymrels5  37363  eltrrels3  37387  eleqvrels3  37400  lpolsetN  40290  islpolN  40291  ismrc  41371  2sbc6g  43106  fun2dmnopgexmpl  45926  joindm2  47502  meetdm2  47504