Theorem 2albii 1830

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 1829	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1829	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Syntax hints:   ↔ wb 208  ∀wal 1548

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

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  3albii  1831  sbcom2  2196  2sb6rf  2494  mo4f  2584  2mo2  2664  2mos  2666  r3al  3190  ralcom  3280  ralcomf  3290  sbccomlem  3813  nfnid  5322  ssrel3  5747  raliunxp  5800  cnvsym  6087  intasym  6088  intirr  6091  codir  6093  qfto  6094  dfpo2  6268  dffun4  6519  fun11  6580  fununi  6581  mpo2eqb  7513  frpoins3xpg  8104  xpord3inddlem  8118  aceq0  10060  zfac  10403  zfcndac  10563  addsrmo  11017  mulsrmo  11018  cotr2g  14975  isirred2  20438  isdomn3  20733  ons2ind  28334  bnj580  35155  bnj978  35191  axacprim  35995  dfso2  36043  dfon2lem8  36076  dffun10  36200  mh-infprim2bi  36845  wl-sbcom2d  38002  mpobi123f  38599  r2alan  38688  inxpss  38754  inxpss3  38757  cnvref5  38788  trcoss2  39011  dfantisymrel5  39302  antisymrelres  39303  dford4  43544  undmrnresiss  44118  cnvssco  44120  pm14.12  44935  permac8prim  45528  ichn  48000  dfich2  48002  ichcom  48003  ichbi12i  48004  pg4cyclnex  48687