Theorem 2albii 1641

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 1640	. 2
3	2	albii 1640	1

Syntax hints:  <->wb 184  A.wal 1393

This theorem is referenced by:  sbcom2  2189  2sb6rf  2196  mo4f  2336  2mo2  2372  2mos  2375  2eu4OLD  2381  2eu6OLD  2384  r3al  2837  ralcomf  3016  nfnid  4681  raliunxp  5147  cnvsym  5386  intasym  5387  intirr  5390  codir  5392  qfto  5393  dffun4  5605  fun11  5658  fununi  5659  mpt22eqb  6411  aceq0  8520  zfac  8861  zfcndac  9018  addsrmo  9471  mulsrmo  9472  isirred2  17350  2spotdisj  25061  rmo4fOLD  27395  axacprim  29079  dfso2  29183  dfpo2  29184  dfon2lem8  29222  dffun10  29564  wl-sbcom2d  30011  mpt2bi123f  30571  dford4  30971  isdomn3  31164  pm14.12  31328  bnj580  33971  bnj978  34007  cotr2g  37786

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

This theorem depends on definitions:  df-bi 185