Theorem 2albii 1915

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

Syntax hints:   ↔ wb 197  ∀wal 1650

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

This theorem depends on definitions:  df-bi 198

This theorem is referenced by:  sbcom2  2536  2sb6rf  2543  mo4f  2636  2mo2  2671  2mos  2673  r3al  3086  ralcomf  3242  nfnid  5010  raliunxp  5429  cnvsym  5692  intasym  5693  intirr  5696  codir  5698  qfto  5699  dffun4  6079  fun11  6140  fununi  6141  mpt22eqb  6966  aceq0  9191  zfac  9534  zfcndac  9693  addsrmo  10146  mulsrmo  10147  cotr2g  14003  isirred2  18967  bnj580  31362  bnj978  31398  axacprim  31961  dfso2  32020  dfpo2  32021  dfon2lem8  32069  dffun10  32396  wl-sbcom2d  33701  mpt2bi123f  34324  3albii  34379  ssrel3  34431  inxpss  34444  inxpss3  34446  trcoss2  34595  eqvrelcoels4  34723  dford4  38205  isdomn3  38391  undmrnresiss  38517  cnvssco  38519  ntrneikb  38998  ntrneixb  38999  pm14.12  39227