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

Theorem 3anbi2d 1257
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 228 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi12d 1253 1  |-  ( ph  ->  ( ( th  /\  ps  /\  ta )  <->  ( th  /\  ch  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  vtocl3gaf  2852  ereq2  6668  isdrngrd  15538  lmodlema  15632  hausnei  17056  regr1lem2  17431  isnvlem  21166  csmdsymi  22914  cvmlift3lem4  23853  cvmlift3  23859  br8  24113  br6  24114  br4  24115  brbtwn  24527  axlowdim  24589  axeuclidlem  24590  brcolinear2  24681  colineardim1  24684  brfs  24702  fscgr  24703  btwnconn1lem7  24716  brsegle  24731  tpssg  24932  isalg  25721  algi  25727  iepiclem  25823  rocatval2  25960  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  sdclem2  26452  sdclem1  26453  sdc  26454  fdc  26455  monotoddzz  27028  jm2.27  27101  mendlmod  27501  fmulcl  27711  fmuldfeqlem1  27712  stoweidlem6  27755  stoweidlem8  27757  stoweidlem31  27780  stoweidlem34  27783  stoweidlem43  27792  stoweidlem51  27800  bnj852  28953  bnj18eq1  28959  bnj938  28969  bnj983  28983  bnj1318  29055  bnj1326  29056  cdleme18d  30484  cdlemk35s  31126  cdlemk39s  31128
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator