Theorem 3anbi3d 1305

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1d.1

Assertion

Ref	Expression
3anbi3d

Proof of Theorem 3anbi3d

Step	Hyp	Ref	Expression
1		biidd 237	. 2
2		3anbi1d.1	. 2
3	1, 2	3anbi13d 1301	1

Syntax hints:  ->wi 4  <->wb 184  /\w3a 973

This theorem is referenced by:  ceqsex3v  3149  ceqsex4v  3150  ceqsex8v  3152  vtocl3gaf  3176  mob  3281  offval22  6879  smogt  7057  cfsmolem  8671  fseq1m1p1  11782  2swrd1eqwrdeq  12679  2swrd2eqwrdeq  12891  prodmo  13743  fprod  13748  divalg  14061  funcres2b  15266  posi  15579  mhmlem  16190  isdrngrd  17422  lmodlema  17517  connsub  19922  lmmbr3  21699  lmmcvg  21700  dvmptfsum  22376  axtg5seg  23862  axtgupdim2  23869  axtgeucl  23870  hlcomb  23987  iscgra  24169  brbtwn  24202  axlowdim  24264  axeuclidlem  24265  1pthoncl  24594  3v3e3cycl1  24644  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  usg2wlkonot  24883  rusgra0edg  24955  2spotdisj  25061  nvi  25507  isslmd  27745  slmdlema  27746  afsval  28551  brafs  28552  cvmlift3lem2  28765  cvmlift3lem4  28767  cvmlift3  28773  frrlem1  29387  brofs  29655  brifs  29693  cgr3permute1  29698  brcolinear2  29708  colineardim1  29711  brfs  29729  btwnconn1  29751  brsegle  29758  iscringd  30396  monotoddzz  30879  jm2.27  30950  mendlmod  31142  fmulcl  31575  fmuldfeqlem1  31576  fmuldfeq  31577  fprodcncf  31704  dvnmptdivc  31735  dvnprodlem2  31744  dvnprodlem3  31745  stoweidlem6  31788  stoweidlem8  31790  stoweidlem26  31808  stoweidlem31  31813  stoweidlem62  31844  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  usgra2pth0  32355  bnj981  34008  bnj1326  34082  oposlem  34907  ishlat1  35077  3dim1lem5  35190  lvoli2  35305  cdlemk42  36667  diclspsn  36921

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  df-3an 975