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

Theorem 3anbi2d 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
3anbi2d  |-  ( ph  ->  ( ( th  /\  ps  /\  ta )  <->  ( th  /\  ch  /\  ta )
) )

Proof of Theorem 3anbi2d
StepHypRef Expression
1 biidd 229 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi12d 1255 1  |-  ( ph  ->  ( ( th  /\  ps  /\  ta )  <->  ( th  /\  ch  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  vtocl3gaf  2965  ereq2  6851  isdrngrd  15790  lmodlema  15884  neiptoptop  17120  neiptopnei  17121  hausnei  17316  regr1lem2  17695  ustuqtop4  18197  utopsnneiplem  18200  isnvlem  21939  csmdsymi  23687  cvmlift3lem4  24790  cvmlift3  24796  br8  25139  br6  25140  br4  25141  brbtwn  25554  axlowdim  25616  axeuclidlem  25617  brcolinear2  25708  colineardim1  25711  brfs  25729  fscgr  25730  btwnconn1lem7  25743  brsegle  25758  sdclem2  26139  sdclem1  26140  sdc  26141  fdc  26142  monotoddzz  26699  jm2.27  26772  mendlmod  27172  fmulcl  27381  fmuldfeqlem1  27382  stoweidlem6  27425  stoweidlem8  27427  stoweidlem31  27450  stoweidlem34  27453  stoweidlem43  27462  stoweidlem52  27471  bnj852  28632  bnj18eq1  28638  bnj938  28648  bnj983  28662  bnj1318  28734  bnj1326  28735  cdleme18d  30411  cdlemk35s  31053  cdlemk39s  31055
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator