MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi2d Unicode version

Theorem 3anbi2d 1304
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1d.1
Assertion
Ref Expression
3anbi2d

Proof of Theorem 3anbi2d
StepHypRef Expression
1 biidd 237 . 2
2 3anbi1d.1 . 2
31, 23anbi12d 1300 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\w3a 973
This theorem is referenced by:  vtocl3gaf  3176  offval22  6879  ereq2  7338  mhmlem  16190  isdrngrd  17422  lmodlema  17517  mdetunilem9  19122  neiptoptop  19632  neiptopnei  19633  hausnei  19829  regr1lem2  20241  ustuqtop4  20747  utopsnneiplem  20750  axtg5seg  23862  axtgupdim2  23869  axtgeucl  23870  brbtwn  24202  axlowdim  24264  axeuclidlem  24265  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  isnvlem  25503  csmdsymi  27253  br8d  27463  slmdlema  27746  sitgclg  28284  cvmlift3lem4  28767  cvmlift3  28773  br8  29185  br6  29186  br4  29187  brcolinear2  29708  colineardim1  29711  brfs  29729  fscgr  29730  btwnconn1lem7  29743  brsegle  29758  sdclem2  30235  sdclem1  30236  sdc  30237  fdc  30238  monotoddzz  30879  jm2.27  30950  mendlmod  31142  fmulcl  31575  fmuldfeqlem1  31576  fprodcncf  31704  dvmptfprodlem  31741  dvmptfprod  31742  dvnprodlem2  31744  stoweidlem6  31788  stoweidlem8  31790  stoweidlem31  31813  stoweidlem34  31816  stoweidlem43  31825  stoweidlem52  31834  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  lmod1  33093  bnj852  33979  bnj18eq1  33985  bnj938  33995  bnj983  34009  bnj1318  34081  bnj1326  34082  cdleme18d  36020  cdlemk35s  36663  cdlemk39s  36665
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
  Copyright terms: Public domain W3C validator