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  1709  cofsmo  7911  axdc3lem3  8094  axdc3lem4  8095  iscatd2  13599  opprsubrg  15582  lsspropd  15790  lmres  17044  cnhaus  17098  regsep2  17120  dishaus  17126  ordthauslem  17127  nconsubb  17165  pthaus  17348  txhaus  17357  xkohaus  17363  regr1lem  17446  methaus  18082  metnrmlem3  18381  pmltpclem1  18824  ex-opab  20835  isnvlem  21182  ajval  21456  adjeu  22485  adjval  22486  adj1  22529  adjeq  22531  cnlnssadj  22676  lt2addrd  23264  xlt2addrd  23268  br8  24184  br6  24185  br4  24186  wfrlem1  24327  wfrlem15  24341  nofulllem5  24431  axeuclidlem  24662  brcgr3  24741  brsegle  24803  fvray  24836  linedegen  24838  fvline  24839  bpolyval  24856  islatalg  25286  isded  25839  dedi  25840  ismonb2  25915  isepib2  25925  prismorcset2  26021  domcatfun  26028  codcatfun  26037  cmppar3  26077  isibg2aa  26215  isibg2aalem1  26216  bosser  26270  isibcg  26294  zindbi  27134  jm2.27  27204  psgnunilem1  27519  stoweidlem43  27895  isopos  29992  hlsuprexch  30192  2llnjN  30378  2lplnj  30431  cdlemk42  31752
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