Theorem 2albidv 1945

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  dff13  7240  xpord2indlem  8129  xpord3inddlem  8136  qliftfun  8786  seqf1o  14058  fi1uzind  14522  brfi1indALT  14525  trclfvcotr  15024  dchrelbas3  27304  isch2  31428  isacycgr1  35501  mclsssvlem  35917  mclsval  35918  mclsax  35924  mclsind  35925  trer  36681  mbfresfi  38170  isass  38350  relcnveq2  38833  elrelscnveq2  39133  elsymrels3  39142  elsymrels5  39144  eltrrels3  39168  eleqvrels3  39181  lpolsetN  42111  islpolN  42112  ismrc  43287  2sbc6g  44996  fun2dmnopgexmpl  47883  joindm2  49594  meetdm2  49596