Theorem 2albidv 1955

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210

This theorem is used by:  dff13  7258  xpord2indlem  8164  xpord3inddlem  8171  qliftfun  8823  seqf1o  14186  fi1uzind  14652  brfi1indALT  14655  trclfvcotr  15162  dchrelbas3  27565  isacycgr1  30752  isch2  31825  mclsssvlem  36327  mclsval  36328  mclsax  36334  mclsind  36335  trer  37104  mbfresfi  38585  isass  38781  relcnveq2  39262  elrelscnveq2  39562  elsymrels3  39571  elsymrels5  39573  eltrrels3  39597  eleqvrels3  39610  lpolsetN  42540  islpolN  42541  ismrc  43712  2sbc6g  45399  fun2dmnopgexmpl  48354  joindm2  50076  meetdm2  50078