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  6631  cfsmolem  8152  fseq1m1p1  11125  divalg  12925  funcres2b  14096  posi  14409  isdrngrd  15863  lmodlema  15957  connsub  17486  lmmbr3  19215  lmmcvg  19216  dvmptfsum  19861  1pthoncl  21594  3v3e3cycl1  21633  nvi  22095  cvmlift3lem2  25009  cvmlift3lem4  25011  cvmlift3  25017  prodmo  25264  fprod  25269  frrlem1  25584  brbtwn  25840  axlowdim  25902  axeuclidlem  25903  brofs  25941  brifs  25979  cgr3permute1  25984  brcolinear2  25994  colineardim1  25997  brfs  26015  btwnconn1  26037  brsegle  26044  iscringd  26611  monotoddzz  27008  jm2.27  27081  mendlmod  27480  fmulcl  27689  fmuldfeqlem1  27690  fmuldfeq  27691  stoweidlem6  27733  stoweidlem8  27735  stoweidlem26  27753  stoweidlem31  27758  stoweidlem62  27789  usgra2pth0  28338  el2wlkonot  28389  el2spthonot  28390  el2spthonot0  28391  usg2wlkonot  28403  2spotdisj  28512  bnj981  29383  bnj1326  29457  oposlem  30043  ishlat1  30212  3dim1lem5  30325  lvoli2  30440  cdlemk42  31800  diclspsn  32054
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator