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  2928  ereq2  6752  isdrngrd  15631  lmodlema  15725  hausnei  17156  regr1lem2  17531  isnvlem  21274  csmdsymi  23022  neiptoptop  23444  neiptopnei  23445  ustuqtop4  23548  utopsnneiplem  23551  cvmlift3lem4  24257  cvmlift3  24263  br8  24671  br6  24672  br4  24673  brbtwn  25086  axlowdim  25148  axeuclidlem  25149  brcolinear2  25240  colineardim1  25243  brfs  25261  fscgr  25262  btwnconn1lem7  25275  brsegle  25290  sdclem2  25776  sdclem1  25777  sdc  25778  fdc  25779  monotoddzz  26351  jm2.27  26424  mendlmod  26824  fmulcl  27034  fmuldfeqlem1  27035  stoweidlem6  27078  stoweidlem8  27080  stoweidlem31  27103  stoweidlem34  27106  stoweidlem43  27115  stoweidlem51  27123  bnj852  28698  bnj18eq1  28704  bnj938  28714  bnj983  28728  bnj1318  28800  bnj1326  28801  cdleme18d  30536  cdlemk35s  31178  cdlemk39s  31180
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