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

Theorem 3anbi13d 1299
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 1297 1  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  3anbi3d  1303  ax12wdemo  1836  f1dom3el3dif  6151  cofsmo  8640  axdc3lem3  8823  axdc3lem4  8824  iscatd2  15170  psgnunilem1  16717  nn0gsumfz  17207  opprsubrg  17645  lsspropd  17858  mdetunilem3  19283  mdetunilem9  19289  smadiadetr  19344  lmres  19968  cnhaus  20022  regsep2  20044  dishaus  20050  ordthauslem  20051  nconsubb  20090  pthaus  20305  txhaus  20314  xkohaus  20320  regr1lem  20406  ustval  20871  methaus  21189  metnrmlem3  21531  pmltpclem1  22026  axtgeucl  24068  cgraid  24371  f1otrge  24377  axeuclidlem  24467  2wlkonot  25067  2spthonot  25068  usg2spthonot0  25091  vdn0frgrav2  25225  vdgn0frgrav2  25226  vdn1frgrav2  25227  vdgn1frgrav2  25228  ex-opab  25355  isnvlem  25701  ajval  25975  adjeu  27006  adjval  27007  adj1  27050  adjeq  27052  cnlnssadj  27197  br8d  27678  lt2addrd  27794  xlt2addrd  27809  measval  28406  br8  29426  br6  29427  br4  29428  wfrlem1  29583  wfrlem15  29597  nofulllem5  29706  brcgr3  29924  brsegle  29986  fvray  30019  linedegen  30021  fvline  30022  zindbi  31121  jm2.27  31189  stoweidlem43  32064  fourierdlem42  32170  usgvad2edg  32783  isopos  35302  hlsuprexch  35502  2llnjN  35688  2lplnj  35741  cdlemk42  37064
  Copyright terms: Public domain W3C validator