Theorem 2albii 1818

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

Syntax hints:   ↔ wb 206  ∀wal 1535

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  3albii  1819  sbcom2  2174  2sb6rf  2481  mo4f  2570  2mo2  2650  2mos  2652  2mosOLD  2653  r3al  3203  ralcom  3295  ralcomf  3308  sbccomlem  3891  nfnid  5393  ssrel3  5810  raliunxp  5864  cnvsym  6144  cnvsymOLD  6145  cnvsymOLDOLD  6146  intasym  6147  intirr  6150  codir  6152  qfto  6153  dfpo2  6327  dffun4  6589  fun11  6652  fununi  6653  mpo2eqb  7582  frpoins3xpg  8181  xpord3inddlem  8195  aceq0  10187  zfac  10529  zfcndac  10688  addsrmo  11142  mulsrmo  11143  cotr2g  15025  isirred2  20447  isdomn3  20737  bnj580  34889  bnj978  34925  axacprim  35669  dfso2  35717  dfon2lem8  35754  dffun10  35878  wl-sbcom2d  37515  mpobi123f  38122  r2alan  38205  inxpss  38267  inxpss3  38270  cnvref5  38307  trcoss2  38440  dfantisymrel5  38718  antisymrelres  38719  dford4  42986  undmrnresiss  43566  cnvssco  43568  pm14.12  44390  ichn  47330  dfich2  47332  ichcom  47333  ichbi12i  47334