Theorem 2albidv 1891

Description: Formula-building rule for two universal quantifiers (deduction rule). (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 1889	. 2 ⊢ (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒))
3	2	albidv 1889	1 ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  dff13  6552  qliftfun  7875  seqf1o  12882  fi1uzind  13317  brfi1indALT  13320  trclfvcotr  13794  dchrelbas3  25008  isch2  28208  mclsssvlem  31585  mclsval  31586  mclsax  31592  mclsind  31593  trer  32435  mbfresfi  33586  isass  33775  relcnveq2  34235  elrelscnveq2  34383  elsymrels3  34440  elsymrels5  34442  lpolsetN  37088  islpolN  37089  ismrc  37581  2sbc6g  38933