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

Theorem 3anbi13d 1256
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 229 . 2  |-  ( ph  ->  ( et  <->  et )
)
3 3anbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
41, 2, 33anbi123d 1254 1  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  3anbi3d  1260  ax11wdemo  1730  cofsmo  8084  axdc3lem3  8267  axdc3lem4  8268  iscatd2  13835  opprsubrg  15818  lsspropd  16022  lmres  17288  cnhaus  17342  regsep2  17364  dishaus  17370  ordthauslem  17371  nconsubb  17409  pthaus  17593  txhaus  17602  xkohaus  17608  regr1lem  17694  ustval  18155  methaus  18442  metnrmlem3  18764  pmltpclem1  19214  ex-opab  21590  isnvlem  21939  ajval  22213  adjeu  23242  adjval  23243  adj1  23286  adjeq  23288  cnlnssadj  23433  lt2addrd  23958  xlt2addrd  23962  measval  24350  br8  25139  br6  25140  br4  25141  wfrlem1  25282  wfrlem15  25296  nofulllem5  25386  axeuclidlem  25617  brcgr3  25696  brsegle  25758  fvray  25791  linedegen  25793  fvline  25794  bpolyval  25811  zindbi  26702  jm2.27  26772  psgnunilem1  27087  stoweidlem43  27462  vdn0frgrav2  27779  vdgn0frgrav2  27780  vdn1frgrav2  27781  vdgn1frgrav2  27782  isopos  29297  hlsuprexch  29497  2llnjN  29683  2lplnj  29736  cdlemk42  31057
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