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

Theorem 3anbi13d 1286
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 1284 1  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 960
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 962
This theorem is referenced by:  3anbi3d  1290  ax12wdemo  1770  f1dom3el3dif  5970  cofsmo  8428  axdc3lem3  8611  axdc3lem4  8612  iscatd2  14604  psgnunilem1  15981  opprsubrg  16812  lsspropd  17022  mdetunilem3  18264  mdetunilem9  18270  smadiadetr  18325  lmres  18748  cnhaus  18802  regsep2  18824  dishaus  18830  ordthauslem  18831  nconsubb  18871  pthaus  19055  txhaus  19064  xkohaus  19070  regr1lem  19156  ustval  19621  methaus  19939  metnrmlem3  20281  pmltpclem1  20776  axtgeucl  22820  f1otrge  22943  axeuclidlem  23033  ex-opab  23464  isnvlem  23813  ajval  24087  adjeu  25118  adjval  25119  adj1  25162  adjeq  25164  cnlnssadj  25309  br8d  25768  lt2addrd  25863  xlt2addrd  25878  slmdlema  26070  measval  26468  br8  27415  br6  27416  br4  27417  wfrlem1  27573  wfrlem15  27587  nofulllem5  27696  brcgr3  27926  brsegle  27988  fvray  28021  linedegen  28023  fvline  28024  zindbi  29134  jm2.27  29204  stoweidlem43  29686  2wlkonot  30232  2spthonot  30233  usg2spthonot0  30256  vdn0frgrav2  30464  vdgn0frgrav2  30465  vdn1frgrav2  30466  vdgn1frgrav2  30467  isopos  32438  hlsuprexch  32638  2llnjN  32824  2lplnj  32877  cdlemk42  34198
  Copyright terms: Public domain W3C validator