MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi2d Structured version   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  3012  ereq2  6905  isdrngrd  15851  lmodlema  15945  neiptoptop  17185  neiptopnei  17186  hausnei  17382  regr1lem2  17762  ustuqtop4  18264  utopsnneiplem  18267  isnvlem  22079  csmdsymi  23827  sitgclg  24646  cvmlift3lem4  24999  cvmlift3  25005  br8  25369  br6  25370  br4  25371  brbtwn  25803  axlowdim  25865  axeuclidlem  25866  brcolinear2  25957  colineardim1  25960  brfs  25978  fscgr  25979  btwnconn1lem7  25992  brsegle  26007  sdclem2  26400  sdclem1  26401  sdc  26402  fdc  26403  monotoddzz  26960  jm2.27  27033  mendlmod  27433  fmulcl  27642  fmuldfeqlem1  27643  stoweidlem6  27686  stoweidlem8  27688  stoweidlem31  27711  stoweidlem34  27714  stoweidlem43  27723  stoweidlem52  27732  usgra2wlkspthlem1  28223  usgra2wlkspthlem2  28224  el2wlkonot  28253  el2spthonot  28254  el2spthonot0  28255  bnj852  29193  bnj18eq1  29199  bnj938  29209  bnj983  29223  bnj1318  29295  bnj1326  29296  cdleme18d  30993  cdlemk35s  31635  cdlemk39s  31637
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