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

Theorem 3anbi1d 1298
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1d.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
3anbi1d  |-  ( ph  ->  ( ( ps  /\  th 
/\  ta )  <->  ( ch  /\ 
th  /\  ta )
) )

Proof of Theorem 3anbi1d
StepHypRef Expression
1 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 biidd 237 . 2  |-  ( ph  ->  ( th  <->  th )
)
31, 23anbi12d 1295 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  ta )  <->  ( ch  /\ 
th  /\  ta )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 968
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 970
This theorem is referenced by:  vtocl3gaf  3175  axdc4uz  12051  sqrval  13022  sqreu  13144  mreexexd  14894  iscatd2  14927  lmodprop2d  17350  neiptopnei  19394  hausnei  19590  isreg2  19639  regr1lem2  19971  ustval  20435  ustuqtop4  20477  axtgupdim2  23592  axtgeucl  23593  brbtwn  23873  ax5seg  23912  axlowdim  23935  axeuclidlem  23936  wlkon  24197  wlkonprop  24199  istrl2  24204  is2wlk  24231  pths  24232  is2wlkonot  24527  is2spthonot  24528  el2wlkonot  24533  el2spthonot  24534  el2spthonot0  24535  2wlkonot3v  24539  2spthonot3v  24540  extwwlkfab  24755  nvi  25171  br8d  27124  xlt2addrd  27234  isslmd  27395  slmdlema  27396  relexpindlem  28525  br8  28750  br6  28751  br4  28752  fvtransport  29247  brcolinear2  29273  colineardim1  29276  fscgr  29295  idinside  29299  brsegle  29323  caures  29845  iscringd  29988  jm2.27  30545  oposlem  33856  cdleme18d  34968
  Copyright terms: Public domain W3C validator