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

Theorem 3anbi13d 1302
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 1300 1  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 974
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 976
This theorem is referenced by:  3anbi3d  1306  ax12wdemo  1817  f1dom3el3dif  6161  cofsmo  8652  axdc3lem3  8835  axdc3lem4  8836  iscatd2  14955  psgnunilem1  16392  nn0gsumfz  16886  opprsubrg  17324  lsspropd  17537  mdetunilem3  18989  mdetunilem9  18995  smadiadetr  19050  lmres  19674  cnhaus  19728  regsep2  19750  dishaus  19756  ordthauslem  19757  nconsubb  19797  pthaus  20012  txhaus  20021  xkohaus  20027  regr1lem  20113  ustval  20578  methaus  20896  metnrmlem3  21238  pmltpclem1  21733  axtgeucl  23742  f1otrge  24047  axeuclidlem  24137  2wlkonot  24737  2spthonot  24738  usg2spthonot0  24761  vdn0frgrav2  24895  vdgn0frgrav2  24896  vdn1frgrav2  24897  vdgn1frgrav2  24898  ex-opab  25025  isnvlem  25375  ajval  25649  adjeu  26680  adjval  26681  adj1  26724  adjeq  26726  cnlnssadj  26871  br8d  27335  lt2addrd  27435  xlt2addrd  27450  measval  28042  br8  29160  br6  29161  br4  29162  wfrlem1  29318  wfrlem15  29332  nofulllem5  29441  brcgr3  29671  brsegle  29733  fvray  29766  linedegen  29768  fvline  29769  zindbi  30857  jm2.27  30925  stoweidlem43  31714  fourierdlem42  31820  usgvad2edg  32249  isopos  34639  hlsuprexch  34839  2llnjN  35025  2lplnj  35078  cdlemk42  36401
  Copyright terms: Public domain W3C validator