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  7209  xpord2indlem  8097  xpord3inddlem  8104  qliftfun  8749  seqf1o  14005  fi1uzind  14469  brfi1indALT  14472  trclfvcotr  14971  dchrelbas3  27201  isch2  31294  isacycgr1  35328  mclsssvlem  35744  mclsval  35745  mclsax  35751  mclsind  35752  trer  36498  mbfresfi  37987  isass  38167  relcnveq2  38650  elrelscnveq2  38950  elsymrels3  38959  elsymrels5  38961  eltrrels3  38985  eleqvrels3  38998  lpolsetN  41928  islpolN  41929  ismrc  43133  2sbc6g  44842  fun2dmnopgexmpl  47732  joindm2  49443  meetdm2  49445