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

Theorem 3anbi1d 1259
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 230 . 2  |-  ( ph  ->  ( th  <->  th )
)
31, 23anbi12d 1256 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  ta )  <->  ( ch  /\ 
th  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ w3a 937
This theorem is referenced by:  vtocl3gaf  3022  axdc4uz  11324  sqrval  12044  sqreu  12166  mreexexd  13875  iscatd2  13908  lmodprop2d  16008  neiptopnei  17198  hausnei  17394  isreg2  17443  regr1lem2  17774  ustval  18234  ustuqtop4  18276  wlkon  21532  wlkonprop  21534  istrl2  21540  is2wlk  21567  pths  21568  nvi  22095  xlt2addrd  24126  relexpindlem  25141  br8  25381  br6  25382  br4  25383  brbtwn  25840  ax5seg  25879  axlowdim  25902  axeuclidlem  25903  fvtransport  25968  brcolinear2  25994  colineardim1  25997  fscgr  26016  idinside  26020  brsegle  26044  caures  26468  iscringd  26611  jm2.27  27081  is2wlkonot  28332  is2spthonot  28333  el2wlkonot  28338  el2spthonot  28339  el2spthonot0  28340  2wlkonot3v  28344  2spthonot3v  28345  oposlem  29983  cdleme18d  31094
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator