Theorem 2albii 1823

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 1822	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1822	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 1798  ax-4 1812

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  3albii  1824  sbcom2  2162  2sb6rf  2474  mo4f  2568  2mo2  2650  2mos  2652  r3al  3120  ralcom  3167  ralcomf  3284  nfnid  5299  ssrel3  5698  raliunxp  5751  cnvsym  6024  intasym  6025  intirr  6028  codir  6030  qfto  6031  dfpo2  6203  dffun4  6452  fun11  6515  fununi  6516  mpo2eqb  7415  aceq0  9883  zfac  10225  zfcndac  10384  addsrmo  10838  mulsrmo  10839  cotr2g  14696  isirred2  19952  bnj580  32902  bnj978  32938  axacprim  33657  dfso2  33731  dfon2lem8  33775  frpoins3xpg  33796  frpoins3xp3g  33797  dffun10  34225  wl-sbcom2d  35725  mpobi123f  36329  inxpss  36454  inxpss3  36456  trcoss2  36609  dford4  40858  isdomn3  41036  undmrnresiss  41219  cnvssco  41221  pm14.12  42046  ichn  44919  dfich2  44921  ichcom  44922  ichbi12i  44923