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

Theorem 3anbi23d 1255
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
3anbi23d  |-  ( ph  ->  ( ( et  /\  ps  /\  th )  <->  ( et  /\  ch  /\  ta )
) )

Proof of Theorem 3anbi23d
StepHypRef Expression
1 biidd 228 . 2  |-  ( ph  ->  ( et  <->  et )
)
2 3anbi12d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
3 3anbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
41, 2, 33anbi123d 1252 1  |-  ( ph  ->  ( ( et  /\  ps  /\  th )  <->  ( et  /\  ch  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  riotasv2dOLD  6350  oeeui  6600  fpwwe2lem5  8256  pwfseqlem4a  8283  pwfseqlem4  8284  divalg  12602  iscatd2  13583  posi  14084  issubg3  14637  lmhmpropd  15826  lbsacsbs  15909  cnhaus  17082  nrmsep  17085  dishaus  17110  ordthauslem  17111  nconsubb  17149  pthaus  17332  txhaus  17341  xkohaus  17347  regr1lem  17430  methaus  18066  metnrmlem3  18365  iscau4  18705  pmltpclem1  18808  dvfsumlem2  19374  aannenlem1  19708  aannenlem2  19709  ex-opab  20819  vci  21104  isvclem  21133  isnvlem  21166  dipass  21423  adj1  22513  adjeq  22515  cnlnssadj  22660  br8  24113  br6  24114  br4  24115  axlowdim  24589  axeuclidlem  24590  fvtransport  24655  brcgr3  24669  brfs  24702  fscgr  24703  btwnconn1lem11  24720  brsegle  24731  fvray  24764  linedegen  24766  fvline  24767  islatalg  25183  vecval1b  25451  vecval3b  25452  vri  25492  tcnvec  25690  isalg  25721  algi  25727  ismonb  25810  isepib  25820  prismorcset2  25918  domcatfun  25925  codcatfun  25934  cmppar3  25974  setiscat  25979  pgapspf2  26053  elhaltdp2  26068  isibg2aa  26112  isibg2aalem2  26114  bosser  26167  isibcg  26191  heiborlem2  26536  ismrc  26776  monotoddzzfi  27027  oddcomabszz  27029  zindbi  27031  rmydioph  27107  pmtrfrn  27400  psgnunilem2  27418  psgnunilem3  27419  stoweidlem31  27780  stoweidlem34  27783  stoweidlem43  27792  stoweidlem48  27797  bnj1154  29029  hlsuprexch  29570  3dim1lem5  29655  lplni2  29726  2llnjN  29756  lvoli2  29770  2lplnj  29809  cdleme18d  30484  cdlemg1cex  30777
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