Theorem 2albii 1843

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

Syntax hints:   ↔ wb 209  ∀wal 1561

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  3albii  1844  sbcom2  2209  2sb6rf  2507  mo4f  2597  2mo2  2677  2mos  2679  r3al  3203  ralcom  3293  ralcomf  3303  sbccomlem  3825  nfnid  5336  ssrel3  5762  raliunxp  5815  cnvsym  6104  intasym  6105  intirr  6108  codir  6110  qfto  6111  dfpo2  6286  dffun4  6538  fun11  6599  fununi  6600  mpo2eqb  7532  frpoins3xpg  8124  xpord3inddlem  8138  aceq0  10090  zfac  10432  zfcndac  10592  addsrmo  11046  mulsrmo  11047  cotr2g  15001  isirred2  20491  isdomn3  20787  ons2ind  28422  bnj580  35213  bnj978  35249  axacprim  36065  dfso2  36113  dfon2lem8  36146  dffun10  36270  mh-infprim2bi  36915  wl-sbcom2d  38071  mpobi123f  38668  r2alan  38757  inxpss  38823  inxpss3  38826  cnvref5  38857  trcoss2  39080  dfantisymrel5  39371  antisymrelres  39372  dford4  43613  undmrnresiss  44187  cnvssco  44189  pm14.12  44990  permac8prim  45582  ichn  48061  dfich2  48063  ichcom  48064  ichbi12i  48065  pg4cyclnex  48748