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

Theorem 3anbi13d 1301
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 1299 1  |-  ( ph  ->  ( ( ps  /\  et  /\  th )  <->  ( ch  /\  et  /\  ta )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973
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 975
This theorem is referenced by:  3anbi3d  1305  ax12wdemo  1780  f1dom3el3dif  6163  cofsmo  8648  axdc3lem3  8831  axdc3lem4  8832  iscatd2  14935  psgnunilem1  16321  nn0gsumfz  16812  opprsubrg  17245  lsspropd  17458  mdetunilem3  18899  mdetunilem9  18905  smadiadetr  18960  lmres  19583  cnhaus  19637  regsep2  19659  dishaus  19665  ordthauslem  19666  nconsubb  19706  pthaus  19890  txhaus  19899  xkohaus  19905  regr1lem  19991  ustval  20456  methaus  20774  metnrmlem3  21116  pmltpclem1  21611  axtgeucl  23614  f1otrge  23867  axeuclidlem  23957  2wlkonot  24557  2spthonot  24558  usg2spthonot0  24581  vdn0frgrav2  24716  vdgn0frgrav2  24717  vdn1frgrav2  24718  vdgn1frgrav2  24719  ex-opab  24846  isnvlem  25195  ajval  25469  adjeu  26500  adjval  26501  adj1  26544  adjeq  26546  cnlnssadj  26691  br8d  27152  lt2addrd  27247  xlt2addrd  27262  slmdlema  27424  measval  27825  br8  28778  br6  28779  br4  28780  wfrlem1  28936  wfrlem15  28950  nofulllem5  29059  brcgr3  29289  brsegle  29351  fvray  29384  linedegen  29386  fvline  29387  zindbi  30502  jm2.27  30570  stoweidlem43  31359  fourierdlem42  31465  usgvad2edg  31894  isopos  33986  hlsuprexch  34186  2llnjN  34372  2lplnj  34425  cdlemk42  35746
  Copyright terms: Public domain W3C validator