Theorem 2albii 1819

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

Syntax hints:   ↔ wb 206  ∀wal 1537

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  3albii  1820  sbcom2  2172  2sb6rf  2476  mo4f  2565  2mo2  2645  2mos  2647  2mosOLD  2648  r3al  3184  ralcom  3273  ralcomf  3285  sbccomlem  3849  nfnid  5355  ssrel3  5776  raliunxp  5830  cnvsym  6112  cnvsymOLD  6113  cnvsymOLDOLD  6114  intasym  6115  intirr  6118  codir  6120  qfto  6121  dfpo2  6296  dffun4  6557  fun11  6620  fununi  6621  mpo2eqb  7547  frpoins3xpg  8147  xpord3inddlem  8161  aceq0  10140  zfac  10482  zfcndac  10641  addsrmo  11095  mulsrmo  11096  cotr2g  14998  isirred2  20390  isdomn3  20684  bnj580  34902  bnj978  34938  axacprim  35682  dfso2  35730  dfon2lem8  35766  dffun10  35890  wl-sbcom2d  37537  mpobi123f  38144  r2alan  38225  inxpss  38287  inxpss3  38290  cnvref5  38327  trcoss2  38460  dfantisymrel5  38738  antisymrelres  38739  dford4  43019  undmrnresiss  43594  cnvssco  43596  pm14.12  44412  ichn  47416  dfich2  47418  ichcom  47419  ichbi12i  47420