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  6366  oeeui  6616  fpwwe2lem5  8272  pwfseqlem4a  8299  pwfseqlem4  8300  divalg  12618  iscatd2  13599  posi  14100  issubg3  14653  lmhmpropd  15842  lbsacsbs  15925  cnhaus  17098  nrmsep  17101  dishaus  17126  ordthauslem  17127  nconsubb  17165  pthaus  17348  txhaus  17357  xkohaus  17363  regr1lem  17446  methaus  18082  metnrmlem3  18381  iscau4  18721  pmltpclem1  18824  dvfsumlem2  19390  aannenlem1  19724  aannenlem2  19725  ex-opab  20835  vci  21120  isvclem  21149  isnvlem  21182  dipass  21439  adj1  22529  adjeq  22531  cnlnssadj  22676  cprodeq2w  24134  cprodeq2ii  24135  br8  24184  br6  24185  br4  24186  axlowdim  24661  axeuclidlem  24662  fvtransport  24727  brcgr3  24741  brfs  24774  fscgr  24775  btwnconn1lem11  24792  brsegle  24803  fvray  24836  linedegen  24838  fvline  24839  islatalg  25286  vecval1b  25554  vecval3b  25555  vri  25595  tcnvec  25793  isalg  25824  algi  25830  ismonb  25913  isepib  25923  prismorcset2  26021  domcatfun  26028  codcatfun  26037  cmppar3  26077  setiscat  26082  pgapspf2  26156  elhaltdp2  26171  isibg2aa  26215  isibg2aalem2  26217  bosser  26270  isibcg  26294  heiborlem2  26639  ismrc  26879  monotoddzzfi  27130  oddcomabszz  27132  zindbi  27134  rmydioph  27210  pmtrfrn  27503  psgnunilem2  27521  psgnunilem3  27522  stoweidlem31  27883  stoweidlem34  27886  stoweidlem43  27895  stoweidlem48  27900  iswlkon  28332  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  bnj1154  29345  hlsuprexch  30192  3dim1lem5  30277  lplni2  30348  2llnjN  30378  lvoli2  30392  2lplnj  30431  cdleme18d  31106  cdlemg1cex  31399
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