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

Theorem 3anbi3d 1258
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 228 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi13d 1254 1  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  ceqsex3v  2902  ceqsex4v  2903  ceqsex8v  2905  vtocl3gaf  2928  mob  3023  smogt  6471  cfsmolem  7986  fseq1m1p1  10950  divalg  12699  funcres2b  13870  posi  14183  isdrngrd  15637  lmodlema  15731  connsub  17253  lmmbr3  18790  lmmcvg  18791  dvmptfsum  19426  nvi  21284  cvmlift3lem2  24255  cvmlift3lem4  24257  cvmlift3  24263  prodmo  24563  fprod  24568  frrlem1  24839  brbtwn  25086  axlowdim  25148  axeuclidlem  25149  brofs  25187  brifs  25225  cgr3permute1  25230  brcolinear2  25240  colineardim1  25243  brfs  25261  btwnconn1  25283  brsegle  25290  bpolylem  25342  iscringd  25947  monotoddzz  26351  jm2.27  26424  mendlmod  26824  fmulcl  27034  fmuldfeqlem1  27035  fmuldfeq  27036  stoweidlem6  27078  stoweidlem8  27080  stoweidlem26  27098  stoweidlem62  27134  1pthoncl  27728  3v3e3cycl1  27768  bnj981  28744  bnj1326  28818  oposlem  29442  ishlat1  29611  3dim1lem5  29724  lvoli2  29839  cdlemk42  31199  diclspsn  31453
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator