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  7275  xpord2indlem  8172  xpord3inddlem  8179  qliftfun  8842  seqf1o  14084  fi1uzind  14546  brfi1indALT  14549  trclfvcotr  15048  dchrelbas3  27282  isch2  31242  isacycgr1  35151  mclsssvlem  35567  mclsval  35568  mclsax  35574  mclsind  35575  trer  36317  mbfresfi  37673  isass  37853  relcnveq2  38324  elrelscnveq2  38494  elsymrels3  38555  elsymrels5  38557  eltrrels3  38581  eleqvrels3  38594  lpolsetN  41484  islpolN  41485  ismrc  42712  2sbc6g  44434  fun2dmnopgexmpl  47296  joindm2  48865  meetdm2  48867