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  2502  mo4f  2592  2mo2  2672  2mos  2674  r3al  3200  ralcom  3290  ralcomf  3300  sbccomlem  3817  nfnid  5340  ssrel3  5766  raliunxp  5819  cnvsym  6108  intasym  6109  intirr  6112  codir  6114  qfto  6115  dfpo2  6294  dffun4  6546  fun11  6607  fununi  6608  mpo2eqb  7545  frpoins3xpg  8138  xpord3inddlem  8152  aceq0  10121  zfac  10462  zfcndac  10628  addsrmo  11082  mulsrmo  11083  cotr2g  15049  isirred2  20562  isdomn3  20876  ons2ind  28540  bnj580  35422  bnj978  35458  axacprim  36286  dfso2  36334  dfon2lem8  36367  dffun10  36491  mh-infprim2bi  37166  wl-sbcom2d  38324  mpobi123f  38910  r2alan  38999  inxpss  39065  inxpss3  39068  cnvref5  39099  trcoss2  39322  dfantisymrel5  39613  antisymrelres  39614  dford4  43870  undmrnresiss  44444  cnvssco  44446  pm14.12  45245  permac8prim  45837  ichn  48356  dfich2  48358  ichcom  48359  ichbi12i  48360  pg4cyclnex  49043