Theorem 2albii 1850

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

Syntax hints:   ↔ wb 209  ∀wal 1568

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  3albii  1851  sbcom2  2207  2sb6rf  2505  mo4f  2595  2mo2  2675  2mos  2677  r3al  3203  ralcom  3293  ralcomf  3303  sbccomlem  3823  nfnid  5348  ssrel3  5774  raliunxp  5827  cnvsym  6116  intasym  6117  intirr  6120  codir  6122  qfto  6123  dfpo2  6299  dffun4  6551  fun11  6612  fununi  6613  mpo2eqb  7544  frpoins3xpg  8137  xpord3inddlem  8151  aceq0  10103  zfac  10445  zfcndac  10605  addsrmo  11059  mulsrmo  11060  cotr2g  15015  isirred2  20504  isdomn3  20800  ons2ind  28449  bnj580  35282  bnj978  35318  axacprim  36180  dfso2  36228  dfon2lem8  36261  dffun10  36385  mh-infprim2bi  37039  wl-sbcom2d  38197  mpobi123f  38792  r2alan  38881  inxpss  38947  inxpss3  38950  cnvref5  38981  trcoss2  39204  dfantisymrel5  39495  antisymrelres  39496  dford4  43739  undmrnresiss  44313  cnvssco  44315  pm14.12  45114  permac8prim  45706  ichn  48188  dfich2  48190  ichcom  48191  ichbi12i  48192  pg4cyclnex  48875