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

Theorem 3anbi3d 1261
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1d.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
3anbi3d  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )

Proof of Theorem 3anbi3d
StepHypRef Expression
1 biidd 230 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi13d 1257 1  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ w3a 937
This theorem is referenced by:  ceqsex3v  2996  ceqsex4v  2997  ceqsex8v  2999  vtocl3gaf  3022  mob  3118  smogt  6632  cfsmolem  8155  fseq1m1p1  11128  divalg  12928  funcres2b  14099  posi  14412  isdrngrd  15866  lmodlema  15960  connsub  17489  lmmbr3  19218  lmmcvg  19219  dvmptfsum  19864  1pthoncl  21597  3v3e3cycl1  21636  nvi  22098  cvmlift3lem2  25012  cvmlift3lem4  25014  cvmlift3  25020  prodmo  25267  fprod  25272  frrlem1  25587  brbtwn  25843  axlowdim  25905  axeuclidlem  25906  brofs  25944  brifs  25982  cgr3permute1  25987  brcolinear2  25997  colineardim1  26000  brfs  26018  btwnconn1  26040  brsegle  26047  iscringd  26623  monotoddzz  27020  jm2.27  27093  mendlmod  27492  fmulcl  27701  fmuldfeqlem1  27702  fmuldfeq  27703  stoweidlem6  27745  stoweidlem8  27747  stoweidlem26  27765  stoweidlem31  27770  stoweidlem62  27801  usgra2pth0  28350  el2wlkonot  28401  el2spthonot  28402  el2spthonot0  28403  usg2wlkonot  28415  2spotdisj  28524  bnj981  29395  bnj1326  29469  oposlem  30055  ishlat1  30224  3dim1lem5  30337  lvoli2  30452  cdlemk42  31812  diclspsn  32066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator