Theorem 2albidv 1921

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  dff13  7275  xpord2indlem  8171  xpord3inddlem  8178  qliftfun  8841  seqf1o  14081  fi1uzind  14543  brfi1indALT  14546  trclfvcotr  15045  dchrelbas3  27297  isch2  31252  isacycgr1  35131  mclsssvlem  35547  mclsval  35548  mclsax  35554  mclsind  35555  trer  36299  mbfresfi  37653  isass  37833  relcnveq2  38305  elrelscnveq2  38475  elsymrels3  38536  elsymrels5  38538  eltrrels3  38562  eleqvrels3  38575  lpolsetN  41465  islpolN  41466  ismrc  42689  2sbc6g  44411  fun2dmnopgexmpl  47234  joindm2  48765  meetdm2  48767