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  2826  ceqsex4v  2827  ceqsex8v  2829  vtocl3gaf  2852  mob  2947  smogt  6384  cfsmolem  7896  fseq1m1p1  10858  divalg  12602  funcres2b  13771  posi  14084  isdrngrd  15538  lmodlema  15632  connsub  17147  lmmbr3  18686  lmmcvg  18687  dvmptfsum  19322  nvi  21170  cvmlift3lem2  23851  cvmlift3lem4  23853  cvmlift3  23859  frrlem1  24281  brbtwn  24527  axlowdim  24589  axeuclidlem  24590  brofs  24628  brifs  24666  cgr3permute1  24671  brcolinear2  24681  colineardim1  24684  brfs  24702  btwnconn1  24724  brsegle  24731  bpolylem  24783  tpssg  24932  islatalg  25183  geme2  25275  vecval1b  25451  vecval3b  25452  fisub  25554  tartarmap  25888  prismorcset  25914  prismorcset2  25918  domcatfun  25925  codcatfun  25934  rocatval2  25960  isibg2  26110  isibg2aa  26112  isibg2aalem2  26114  isibcg  26191  iscringd  26624  monotoddzz  27028  jm2.27  27101  mendlmod  27501  fmulcl  27711  fmuldfeqlem1  27712  fmuldfeq  27713  stoweidlem6  27755  stoweidlem8  27757  stoweidlem26  27775  stoweidlem62  27811  bnj981  28982  bnj1326  29056  oposlem  29373  ishlat1  29542  3dim1lem5  29655  lvoli2  29770  cdlemk42  31130  diclspsn  31384
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