Theorem 2albidv 1952

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 1949	. 2 ⊢ (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
3	2	albidv 1949	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 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210

This theorem is used by:  dff13  7252  xpord2indlem  8141  xpord3inddlem  8148  qliftfun  8798  seqf1o  14086  fi1uzind  14551  brfi1indALT  14554  trclfvcotr  15053  dchrelbas3  27413  isch2  31586  isacycgr1  35646  mclsssvlem  36062  mclsval  36063  mclsax  36069  mclsind  36070  trer  36855  mbfresfi  38345  isass  38525  relcnveq2  39006  elrelscnveq2  39306  elsymrels3  39315  elsymrels5  39317  eltrrels3  39341  eleqvrels3  39354  lpolsetN  42284  islpolN  42285  ismrc  43460  2sbc6g  45153  fun2dmnopgexmpl  48049  joindm2  49774  meetdm2  49776