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  7254  xpord2indlem  8133  xpord3inddlem  8140  qliftfun  8796  seqf1o  14009  fi1uzind  14458  brfi1indALT  14461  trclfvcotr  14956  dchrelbas3  26741  isch2  30476  isacycgr1  34137  mclsssvlem  34553  mclsval  34554  mclsax  34560  mclsind  34561  trer  35201  mbfresfi  36534  isass  36714  relcnveq2  37192  elrelscnveq2  37363  elsymrels3  37424  elsymrels5  37426  eltrrels3  37450  eleqvrels3  37463  lpolsetN  40353  islpolN  40354  ismrc  41439  2sbc6g  43174  fun2dmnopgexmpl  45992  joindm2  47601  meetdm2  47603