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

Theorem 3anbi13d 1345
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 245 . 2  |-  ( ph  ->  ( et  <->  et )
)
3 3anbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
41, 2, 33anbi123d 1343 1  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ w3a 986
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 190  df-an 377  df-3an 988
This theorem is referenced by:  3anbi3d  1349  ax12wdemo  1912  f1dom3el3dif  6154  wfrlem1  7021  wfrlem3a  7024  wfrlem15  7036  cofsmo  8685  axdc3lem3  8868  axdc3lem4  8869  iscatd2  15597  psgnunilem1  17144  nn0gsumfz  17623  opprsubrg  18039  lsspropd  18250  mdetunilem3  19649  mdetunilem9  19655  smadiadetr  19710  lmres  20326  cnhaus  20380  regsep2  20402  dishaus  20408  ordthauslem  20409  nconsubb  20448  pthaus  20663  txhaus  20672  xkohaus  20678  regr1lem  20764  ustval  21227  methaus  21545  metnrmlem3  21888  metnrmlem3OLD  21903  pmltpclem1  22409  axtgeucl  24531  iscgrad  24864  dfcgra2  24882  f1otrge  24913  axeuclidlem  25003  2wlkonot  25604  2spthonot  25605  usg2spthonot0  25628  vdn0frgrav2  25762  vdgn0frgrav2  25763  vdn1frgrav2  25764  vdgn1frgrav2  25765  ex-opab  25893  isnvlem  26240  ajval  26514  adjeu  27553  adjval  27554  adj1  27597  adjeq  27599  cnlnssadj  27744  br8d  28226  lt2addrd  28333  xlt2addrd  28345  measval  29026  br8  30401  br6  30402  br4  30403  nofulllem5  30600  brcgr3  30818  brsegle  30880  fvray  30913  linedegen  30915  fvline  30916  poimirlem28  31969  isopos  32747  hlsuprexch  32947  2llnjN  33133  2lplnj  33186  cdlemk42  34509  zindbi  35795  jm2.27  35864  stoweidlem43  37960  fourierdlem42  38068  fourierdlem42OLD  38069  upgr3v3e3cycl  39972  upgr4cycl4dv4e  39977  usgvad2edg  40047
  Copyright terms: Public domain W3C validator