Theorem 2albii 1815

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

Syntax hints:   ↔ wb 205  ∀wal 1532

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  3albii  1816  sbcom2  2163  2sb6rf  2468  mo4f  2557  2mo2  2639  2mos  2641  r3al  3192  ralcom  3282  ralcomf  3295  nfnid  5369  ssrel3  5782  raliunxp  5836  cnvsym  6112  cnvsymOLD  6113  cnvsymOLDOLD  6114  intasym  6115  intirr  6118  codir  6120  qfto  6121  dfpo2  6294  dffun4  6558  fun11  6621  fununi  6622  mpo2eqb  7547  frpoins3xpg  8139  xpord3inddlem  8153  aceq0  10135  zfac  10477  zfcndac  10636  addsrmo  11090  mulsrmo  11091  cotr2g  14949  isirred2  20353  isdomn3  21241  bnj580  34538  bnj978  34574  axacprim  35295  dfso2  35343  dfon2lem8  35380  dffun10  35504  wl-sbcom2d  37022  mpobi123f  37629  r2alan  37714  inxpss  37777  inxpss3  37780  cnvref5  37817  trcoss2  37950  dfantisymrel5  38228  antisymrelres  38229  dford4  42444  undmrnresiss  43028  cnvssco  43030  pm14.12  43852  ichn  46790  dfich2  46792  ichcom  46793  ichbi12i  46794