Theorem 2albidv 1925

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  dff13  7204  xpord2indlem  8092  xpord3inddlem  8099  qliftfun  8744  seqf1o  14000  fi1uzind  14464  brfi1indALT  14467  trclfvcotr  14966  dchrelbas3  27219  isch2  31313  isacycgr1  35348  mclsssvlem  35764  mclsval  35765  mclsax  35771  mclsind  35772  trer  36518  mbfresfi  38007  isass  38187  relcnveq2  38670  elrelscnveq2  38970  elsymrels3  38979  elsymrels5  38981  eltrrels3  39005  eleqvrels3  39018  lpolsetN  41948  islpolN  41949  ismrc  43153  2sbc6g  44866  fun2dmnopgexmpl  47750  joindm2  49461  meetdm2  49463