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

Theorem 3anbi23d 1257
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 229 . 2  |-  ( ph  ->  ( et  <->  et )
)
2 3anbi12d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
3 3anbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
41, 2, 33anbi123d 1254 1  |-  ( ph  ->  ( ( et  /\  ps  /\  th )  <->  ( et  /\  ch  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  riotasv2dOLD  6595  oeeui  6845  fpwwe2lem5  8509  pwfseqlem4a  8536  pwfseqlem4  8537  divalg  12923  iscatd2  13906  posi  14407  issubg3  14960  lmhmpropd  16145  lbsacsbs  16228  neiptoptop  17195  neiptopnei  17196  cnhaus  17418  nrmsep  17421  dishaus  17446  ordthauslem  17447  nconsubb  17486  pthaus  17670  txhaus  17679  xkohaus  17685  regr1lem  17771  isust  18233  ustuqtop4  18274  methaus  18550  metnrmlem3  18891  iscau4  19232  pmltpclem1  19345  dvfsumlem2  19911  aannenlem1  20245  aannenlem2  20246  wlkon  21530  3v3e3cycl1  21631  4cycl4v4e  21653  4cycl4dv4e  21655  ex-opab  21740  vci  22027  isvclem  22056  isnvlem  22089  dipass  22346  adj1  23436  adjeq  23438  cnlnssadj  23583  prodeq2w  25238  prodeq2ii  25239  br8  25379  br6  25380  br4  25381  wrecseq123  25532  axlowdim  25900  axeuclidlem  25901  fvtransport  25966  brcgr3  25980  brfs  26013  fscgr  26014  btwnconn1lem11  26031  brsegle  26042  fvray  26075  linedegen  26077  fvline  26078  heiborlem2  26521  ismrc  26755  monotoddzzfi  27005  oddcomabszz  27007  zindbi  27009  rmydioph  27085  pmtrfrn  27377  psgnunilem2  27395  psgnunilem3  27396  stoweidlem31  27756  stoweidlem34  27759  stoweidlem43  27768  stoweidlem48  27773  swrdccatin12lem4  28213  cshwssizelem2  28281  wlkelwrd  28295  bnj1154  29368  hlsuprexch  30178  3dim1lem5  30263  lplni2  30334  2llnjN  30364  lvoli2  30378  2lplnj  30417  cdleme18d  31092  cdlemg1cex  31385
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator