Theorem 2albidv 1918

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  dff13  7246  xpord2indlem  8127  xpord3inddlem  8134  qliftfun  8792  seqf1o  14006  fi1uzind  14455  brfi1indALT  14458  trclfvcotr  14953  dchrelbas3  27087  isch2  30945  isacycgr1  34626  mclsssvlem  35042  mclsval  35043  mclsax  35049  mclsind  35050  trer  35691  mbfresfi  37024  isass  37204  relcnveq2  37682  elrelscnveq2  37853  elsymrels3  37914  elsymrels5  37916  eltrrels3  37940  eleqvrels3  37953  lpolsetN  40843  islpolN  40844  ismrc  41928  2sbc6g  43663  fun2dmnopgexmpl  46477  joindm2  47789  meetdm2  47791