Theorem 2albidv 1931

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  dff13  7202  xpord2indlem  8091  xpord3inddlem  8098  qliftfun  8743  seqf1o  14000  fi1uzind  14464  brfi1indALT  14467  trclfvcotr  14966  dchrelbas3  27223  isch2  31316  isacycgr1  35389  mclsssvlem  35805  mclsval  35806  mclsax  35812  mclsind  35813  trer  36559  mbfresfi  38048  isass  38228  relcnveq2  38711  elrelscnveq2  39011  elsymrels3  39020  elsymrels5  39022  eltrrels3  39046  eleqvrels3  39059  lpolsetN  41989  islpolN  41990  ismrc  43165  2sbc6g  44874  fun2dmnopgexmpl  47761  joindm2  49472  meetdm2  49474