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

Theorem 3anbi3d 1260
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 229 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi13d 1256 1  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  ceqsex3v  2954  ceqsex4v  2955  ceqsex8v  2957  vtocl3gaf  2980  mob  3076  smogt  6588  cfsmolem  8106  fseq1m1p1  11078  divalg  12878  funcres2b  14049  posi  14362  isdrngrd  15816  lmodlema  15910  connsub  17437  lmmbr3  19166  lmmcvg  19167  dvmptfsum  19812  1pthoncl  21545  3v3e3cycl1  21584  nvi  22046  cvmlift3lem2  24960  cvmlift3lem4  24962  cvmlift3  24968  prodmo  25215  fprod  25220  frrlem1  25495  brbtwn  25742  axlowdim  25804  axeuclidlem  25805  brofs  25843  brifs  25881  cgr3permute1  25886  brcolinear2  25896  colineardim1  25899  brfs  25917  btwnconn1  25939  brsegle  25946  bpolylem  25998  iscringd  26499  monotoddzz  26896  jm2.27  26969  mendlmod  27369  fmulcl  27578  fmuldfeqlem1  27579  fmuldfeq  27580  stoweidlem6  27622  stoweidlem8  27624  stoweidlem26  27642  stoweidlem31  27647  stoweidlem62  27678  usgra2pth0  28042  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  usg2wlkonot  28080  2spotdisj  28164  bnj981  29027  bnj1326  29101  oposlem  29666  ishlat1  29835  3dim1lem5  29948  lvoli2  30063  cdlemk42  31423  diclspsn  31677
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