Theorem 2albii 1853

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210

This theorem is used by:  3albii  1854  sbcom2  2209  2sb6rf  2503  mo4f  2593  2mo2  2673  2mos  2675  r3al  3201  ralcom  3291  ralcomf  3301  sbccomlem  3817  nfnid  5337  ssrel3  5762  raliunxp  5816  cnvsym  6108  intasym  6109  intirr  6112  codir  6114  qfto  6115  dfpo2  6298  dffun4  6550  fun11  6612  fununi  6613  mpo2eqb  7550  frpoins3xpg  8150  xpord3inddlem  8164  aceq0  10190  zfac  10531  zfcndac  10697  addsrmo  11151  mulsrmo  11152  cotr2g  15122  isirred2  20644  isdomn3  20959  ons2ind  28654  bnj580  35536  bnj978  35572  axacprim  36451  dfso2  36499  dfon2lem8  36532  dffun10  36656  mh-infprim2bi  37315  wl-sbcom2d  38473  mpobi123f  39074  r2alan  39163  inxpss  39229  inxpss3  39232  cnvref5  39263  trcoss2  39486  dfantisymrel5  39777  antisymrelres  39778  dford4  44015  undmrnresiss  44589  cnvssco  44591  pm14.12  45390  permac8prim  45982  ichn  48507  dfich2  48509  ichcom  48510  ichbi12i  48511  pg4cyclnex  49194