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  7229  xpord2indlem  8126  xpord3inddlem  8133  qliftfun  8775  seqf1o  14008  fi1uzind  14472  brfi1indALT  14475  trclfvcotr  14975  dchrelbas3  27149  isch2  31152  isacycgr1  35133  mclsssvlem  35549  mclsval  35550  mclsax  35556  mclsind  35557  trer  36304  mbfresfi  37660  isass  37840  relcnveq2  38311  elrelscnveq2  38484  elsymrels3  38545  elsymrels5  38547  eltrrels3  38571  eleqvrels3  38584  lpolsetN  41476  islpolN  41477  ismrc  42689  2sbc6g  44404  fun2dmnopgexmpl  47285  joindm2  48956  meetdm2  48958