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  2839  ceqsex4v  2840  ceqsex8v  2842  vtocl3gaf  2865  mob  2960  smogt  6400  cfsmolem  7912  fseq1m1p1  10874  divalg  12618  funcres2b  13787  posi  14100  isdrngrd  15554  lmodlema  15648  connsub  17163  lmmbr3  18702  lmmcvg  18703  dvmptfsum  19338  nvi  21186  cvmlift3lem2  23866  cvmlift3lem4  23868  cvmlift3  23874  prodmo  24159  fprod  24164  frrlem1  24352  brbtwn  24599  axlowdim  24661  axeuclidlem  24662  brofs  24700  brifs  24738  cgr3permute1  24743  brcolinear2  24753  colineardim1  24756  brfs  24774  btwnconn1  24796  brsegle  24803  bpolylem  24855  tpssg  25035  islatalg  25286  geme2  25378  vecval1b  25554  vecval3b  25555  fisub  25657  tartarmap  25991  prismorcset  26017  prismorcset2  26021  domcatfun  26028  codcatfun  26037  rocatval2  26063  isibg2  26213  isibg2aa  26215  isibg2aalem2  26217  isibcg  26294  iscringd  26727  monotoddzz  27131  jm2.27  27204  mendlmod  27604  fmulcl  27814  fmuldfeqlem1  27815  fmuldfeq  27816  stoweidlem6  27858  stoweidlem8  27860  stoweidlem26  27878  stoweidlem62  27914  3v3e3cycl1  28390  bnj981  29298  bnj1326  29372  oposlem  29995  ishlat1  30164  3dim1lem5  30277  lvoli2  30392  cdlemk42  31752  diclspsn  32006
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