Theorem 2albii 1896

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

Syntax hints:   ↔ wb 196  ∀wal 1629

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

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  sbcom2  2593  2sb6rf  2600  mo4f  2665  2mo2  2699  2mos  2701  r3al  3089  ralcomf  3244  nfnid  5025  raliunxp  5400  cnvsym  5651  intasym  5652  intirr  5655  codir  5657  qfto  5658  dffun4  6043  fun11  6103  fununi  6104  mpt22eqb  6916  aceq0  9141  zfac  9484  zfcndac  9643  addsrmo  10096  mulsrmo  10097  cotr2g  13925  isirred2  18909  rmo4fOLD  29675  bnj580  31321  bnj978  31357  axacprim  31922  dfso2  31982  dfpo2  31983  dfon2lem8  32031  dffun10  32358  wl-sbcom2d  33678  mpt2bi123f  34303  3albii  34356  ssrel3  34410  inxpss  34425  inxpss3  34427  trcoss2  34576  dford4  38122  isdomn3  38308  undmrnresiss  38436  cnvssco  38438  ntrneikb  38918  ntrneixb  38919  pm14.12  39148