Theorem 2albii 1852

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210

This theorem is used by:  3albii  1853  sbcom2  2208  2sb6rf  2502  mo4f  2592  2mo2  2672  2mos  2674  r3al  3200  ralcom  3290  ralcomf  3300  sbccomlem  3816  nfnid  5336  ssrel3  5761  raliunxp  5815  cnvsym  6107  intasym  6108  intirr  6111  codir  6113  qfto  6114  dfpo2  6299  dffun4  6552  fun11  6615  fununi  6616  mpo2eqb  7553  frpoins3xpg  8160  xpord3inddlem  8174  aceq0  10201  zfac  10542  zfcndac  10708  addsrmo  11162  mulsrmo  11163  cotr2g  15135  isirred2  20657  isdomn3  20972  ons2ind  28667  bnj580  35590  bnj978  35626  axacprim  36565  dfso2  36613  dfon2lem8  36645  dffun10  36769  mh-infprim2bi  37428  wl-sbcom2d  38587  mpobi123f  39188  r2alan  39277  inxpss  39343  inxpss3  39346  cnvref5  39377  trcoss2  39600  dfantisymrel5  39891  antisymrelres  39892  dford4  44130  undmrnresiss  44698  cnvssco  44700  pm14.12  45499  permac8prim  46098  ichn  48632  dfich2  48634  ichcom  48635  ichbi12i  48636  pg4cyclnex  49319