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 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  dff13  7109  qliftfun  8549  seqf1o  13692  fi1uzind  14139  brfi1indALT  14142  trclfvcotr  14648  dchrelbas3  26291  isch2  29486  isacycgr1  33008  mclsssvlem  33424  mclsval  33425  mclsax  33431  mclsind  33432  xpord2ind  33721  xpord3ind  33727  trer  34432  mbfresfi  35750  isass  35931  relcnveq2  36385  elrelscnveq2  36538  elsymrels3  36595  elsymrels5  36597  eltrrels3  36621  eleqvrels3  36633  lpolsetN  39423  islpolN  39424  ismrc  40439  2sbc6g  41922  fun2dmnopgexmpl  44663  joindm2  46150  meetdm2  46152