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  2962  ceqsex4v  2963  ceqsex8v  2965  vtocl3gaf  2988  mob  3084  smogt  6596  cfsmolem  8114  fseq1m1p1  11086  divalg  12886  funcres2b  14057  posi  14370  isdrngrd  15824  lmodlema  15918  connsub  17445  lmmbr3  19174  lmmcvg  19175  dvmptfsum  19820  1pthoncl  21553  3v3e3cycl1  21592  nvi  22054  cvmlift3lem2  24968  cvmlift3lem4  24970  cvmlift3  24976  prodmo  25223  fprod  25228  frrlem1  25503  brbtwn  25750  axlowdim  25812  axeuclidlem  25813  brofs  25851  brifs  25889  cgr3permute1  25894  brcolinear2  25904  colineardim1  25907  brfs  25925  btwnconn1  25947  brsegle  25954  bpolylem  26006  iscringd  26507  monotoddzz  26904  jm2.27  26977  mendlmod  27377  fmulcl  27586  fmuldfeqlem1  27587  fmuldfeq  27588  stoweidlem6  27630  stoweidlem8  27632  stoweidlem26  27650  stoweidlem31  27655  stoweidlem62  27686  usgra2pth0  28050  el2wlkonot  28074  el2spthonot  28075  el2spthonot0  28076  usg2wlkonot  28088  2spotdisj  28172  bnj981  29039  bnj1326  29113  oposlem  29678  ishlat1  29847  3dim1lem5  29960  lvoli2  30075  cdlemk42  31435  diclspsn  31689
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