Theorem 2albii 1824

Description: Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)

Hypothesis

Ref	Expression
albii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2albii	⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Proof of Theorem 2albii

Step	Hyp	Ref	Expression
1		albii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	albii 1823	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1823	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Syntax hints:   ↔ wb 205  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  sbcom2  2163  2sb6rf  2473  mo4f  2567  2mo2  2649  2mos  2651  r3al  3125  ralcom  3280  ralcomf  3282  nfnid  5293  raliunxp  5737  cnvsym  6008  intasym  6009  intirr  6012  codir  6014  qfto  6015  dfpo2  6188  dffun4  6430  fun11  6492  fununi  6493  mpo2eqb  7384  aceq0  9805  zfac  10147  zfcndac  10306  addsrmo  10760  mulsrmo  10761  cotr2g  14615  isirred2  19858  bnj580  32793  bnj978  32829  axacprim  33548  dfso2  33628  dfon2lem8  33672  frpoins3xpg  33714  frpoins3xp3g  33715  dffun10  34143  wl-sbcom2d  35643  mpobi123f  36247  3albii  36314  ssrel3  36361  inxpss  36374  inxpss3  36376  trcoss2  36529  dford4  40767  isdomn3  40945  undmrnresiss  41101  cnvssco  41103  pm14.12  41928  ichn  44796  dfich2  44798  ichcom  44799  ichbi12i  44800