Theorem bi2anan9 873

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)

Hypotheses

Ref	Expression
bi2an9.1
bi2an9.2

Assertion

Ref	Expression
bi2anan9

Proof of Theorem bi2anan9

Step	Hyp	Ref	Expression
1		bi2an9.1	. . 3
2	1	anbi1d 704	. 2
3		bi2an9.2	. . 3
4	3	anbi2d 703	. 2
5	2, 4	sylan9bb 699	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  bi2anan9r  874  2eu6OLD  2384  2reu5  3308  ralprg  4078  raltpg  4080  prssg  4185  prsspwg  4187  opelopab2a  4767  opelxp  5034  eqrel  5097  eqrelrel  5109  brcog  5174  dff13  6166  resoprab2  6399  ovig  6424  dfoprab4f  6858  f1o2ndf1  6908  om00el  7244  oeoe  7267  eroveu  7425  endisj  7624  infxpen  8413  dfac5lem4  8528  sornom  8678  ltsrpr  9475  axcnre  9562  axmulgt0  9680  wloglei  10110  mulge0b  10437  addltmul  10799  ltxr  11353  sumsqeq0  12246  rlim  13318  cpnnen  13962  dvds2lem  13996  gcddvds  14153  opoe  14335  omoe  14336  opeo  14337  omeo  14338  pcqmul  14377  xpsfrnel2  14962  eqgval  16250  frgpuplem  16790  mpfind  18205  2ndcctbss  19956  txbasval  20107  cnmpt12  20168  cnmpt22  20175  prdsxmslem2  21032  ishtpy  21472  bcthlem1  21763  bcth  21768  volun  21955  vitali  22022  itg1addlem3  22105  rolle  22391  mumullem2  23454  lgsquadlem3  23631  lgsquad  23632  2sqlem7  23645  axpasch  24244  usgra2adedgwlkonALT  24616  usgra2wlkspthlem1  24619  el2wlkonotot1  24874  frg2wot1  25057  frg2woteqm  25059  numclwwlkovg  25087  hlimi  26105  leopadd  27051  eqrelrd2  27467  isinftm  27725  metidv  27871  altopthg  29617  altopthbg  29618  brsegle  29758  itg2addnclem3  30068  fzadd2  30234  prtlem13  30609  pellex  30771  tpres  32554  dib1dim  36892

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

This theorem depends on definitions:  df-bi 185  df-an 371