Theorem 2albidv 1923

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  dff13  7232  xpord2indlem  8129  xpord3inddlem  8136  qliftfun  8778  seqf1o  14015  fi1uzind  14479  brfi1indALT  14482  trclfvcotr  14982  dchrelbas3  27156  isch2  31159  isacycgr1  35140  mclsssvlem  35556  mclsval  35557  mclsax  35563  mclsind  35564  trer  36311  mbfresfi  37667  isass  37847  relcnveq2  38318  elrelscnveq2  38491  elsymrels3  38552  elsymrels5  38554  eltrrels3  38578  eleqvrels3  38591  lpolsetN  41483  islpolN  41484  ismrc  42696  2sbc6g  44411  fun2dmnopgexmpl  47289  joindm2  48960  meetdm2  48962