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

Theorem 3anbi13d 1254
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
Hypotheses
Ref Expression
3anbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3anbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
3anbi13d  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )

Proof of Theorem 3anbi13d
StepHypRef Expression
1 3anbi12d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 biidd 228 . 2  |-  ( ph  ->  ( et  <->  et )
)
3 3anbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
41, 2, 33anbi123d 1252 1  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  3anbi3d  1258  ax11wdemo  1697  cofsmo  7895  axdc3lem3  8078  axdc3lem4  8079  iscatd2  13583  opprsubrg  15566  lsspropd  15774  lmres  17028  cnhaus  17082  regsep2  17104  dishaus  17110  ordthauslem  17111  nconsubb  17149  pthaus  17332  txhaus  17341  xkohaus  17347  regr1lem  17430  methaus  18066  metnrmlem3  18365  pmltpclem1  18808  ex-opab  20819  isnvlem  21166  ajval  21440  adjeu  22469  adjval  22470  adj1  22513  adjeq  22515  cnlnssadj  22660  lt2addrd  23249  xlt2addrd  23253  br8  24113  br6  24114  br4  24115  wfrlem1  24256  wfrlem15  24270  nofulllem5  24360  axeuclidlem  24590  brcgr3  24669  brsegle  24731  fvray  24764  linedegen  24766  fvline  24767  bpolyval  24784  islatalg  25183  isded  25736  dedi  25737  ismonb2  25812  isepib2  25822  prismorcset2  25918  domcatfun  25925  codcatfun  25934  cmppar3  25974  isibg2aa  26112  isibg2aalem1  26113  bosser  26167  isibcg  26191  zindbi  27031  jm2.27  27101  psgnunilem1  27416  stoweidlem43  27792  isopos  29370  hlsuprexch  29570  2llnjN  29756  2lplnj  29809  cdlemk42  31130
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