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

Theorem 3anbi13d 1291
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 237 . 2  |-  ( ph  ->  ( et  <->  et )
)
3 3anbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
41, 2, 33anbi123d 1289 1  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  3anbi3d  1295  ax12wdemo  1769  f1dom3el3dif  5981  cofsmo  8438  axdc3lem3  8621  axdc3lem4  8622  iscatd2  14619  psgnunilem1  15999  opprsubrg  16886  lsspropd  17098  mdetunilem3  18420  mdetunilem9  18426  smadiadetr  18481  lmres  18904  cnhaus  18958  regsep2  18980  dishaus  18986  ordthauslem  18987  nconsubb  19027  pthaus  19211  txhaus  19220  xkohaus  19226  regr1lem  19312  ustval  19777  methaus  20095  metnrmlem3  20437  pmltpclem1  20932  axtgeucl  22933  f1otrge  23118  axeuclidlem  23208  ex-opab  23639  isnvlem  23988  ajval  24262  adjeu  25293  adjval  25294  adj1  25337  adjeq  25339  cnlnssadj  25484  br8d  25942  lt2addrd  26036  xlt2addrd  26051  slmdlema  26219  measval  26612  br8  27566  br6  27567  br4  27568  wfrlem1  27724  wfrlem15  27738  nofulllem5  27847  brcgr3  28077  brsegle  28139  fvray  28172  linedegen  28174  fvline  28175  zindbi  29287  jm2.27  29357  stoweidlem43  29838  2wlkonot  30384  2spthonot  30385  usg2spthonot0  30408  vdn0frgrav2  30616  vdgn0frgrav2  30617  vdn1frgrav2  30618  vdgn1frgrav2  30619  nn0gsumfz  30804  isopos  32825  hlsuprexch  33025  2llnjN  33211  2lplnj  33264  cdlemk42  34585
  Copyright terms: Public domain W3C validator