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

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

Proof of Theorem 3anbi1d
StepHypRef Expression
1 3anbi1d.1 . 2
2 biidd 237 . 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  axdc4uz  12093  sqrtval  13070  sqreu  13193  mreexexd  15045  iscatd2  15078  lmodprop2d  17572  neiptopnei  19633  hausnei  19829  isreg2  19878  regr1lem2  20241  ustval  20705  ustuqtop4  20747  axtgupdim2  23869  axtgeucl  23870  brbtwn  24202  ax5seg  24241  axlowdim  24264  axeuclidlem  24265  wlkon  24533  wlkonprop  24535  istrl2  24540  is2wlk  24567  pths  24568  is2wlkonot  24863  is2spthonot  24864  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  2wlkonot3v  24875  2spthonot3v  24876  extwwlkfab  25090  nvi  25507  br8d  27463  xlt2addrd  27578  isslmd  27745  slmdlema  27746  relexpindlem  29062  br8  29185  br6  29186  br4  29187  fvtransport  29682  brcolinear2  29708  colineardim1  29711  fscgr  29730  idinside  29734  brsegle  29758  caures  30253  iscringd  30396  jm2.27  30950  oposlem  34907  cdleme18d  36020
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