Theorem 2albidv 1926

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  dff13  7128  qliftfun  8591  seqf1o  13764  fi1uzind  14211  brfi1indALT  14214  trclfvcotr  14720  dchrelbas3  26386  isch2  29585  isacycgr1  33108  mclsssvlem  33524  mclsval  33525  mclsax  33531  mclsind  33532  xpord2ind  33794  xpord3ind  33800  trer  34505  mbfresfi  35823  isass  36004  relcnveq2  36458  elrelscnveq2  36611  elsymrels3  36668  elsymrels5  36670  eltrrels3  36694  eleqvrels3  36706  lpolsetN  39496  islpolN  39497  ismrc  40523  2sbc6g  42033  fun2dmnopgexmpl  44776  joindm2  46262  meetdm2  46264