Theorem 2albidv 1922

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  dff13  7292  xpord2indlem  8188  xpord3inddlem  8195  qliftfun  8860  seqf1o  14094  fi1uzind  14556  brfi1indALT  14559  trclfvcotr  15058  dchrelbas3  27300  isch2  31255  isacycgr1  35114  mclsssvlem  35530  mclsval  35531  mclsax  35537  mclsind  35538  trer  36282  mbfresfi  37626  isass  37806  relcnveq2  38279  elrelscnveq2  38449  elsymrels3  38510  elsymrels5  38512  eltrrels3  38536  eleqvrels3  38549  lpolsetN  41439  islpolN  41440  ismrc  42657  2sbc6g  44384  fun2dmnopgexmpl  47199  joindm2  48648  meetdm2  48650