Theorem 2albidv 1923

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  dff13  7247  xpord2indlem  8146  xpord3inddlem  8153  qliftfun  8816  seqf1o  14061  fi1uzind  14525  brfi1indALT  14528  trclfvcotr  15028  dchrelbas3  27201  isch2  31204  isacycgr1  35168  mclsssvlem  35584  mclsval  35585  mclsax  35591  mclsind  35592  trer  36334  mbfresfi  37690  isass  37870  relcnveq2  38341  elrelscnveq2  38511  elsymrels3  38572  elsymrels5  38574  eltrrels3  38598  eleqvrels3  38611  lpolsetN  41501  islpolN  41502  ismrc  42724  2sbc6g  44439  fun2dmnopgexmpl  47313  joindm2  48942  meetdm2  48944