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

Theorem 3anbi12d 1300
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
3anbi12d  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  et )
) )

Proof of Theorem 3anbi12d
StepHypRef Expression
1 3anbi12d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 3anbi12d.2 . 2  |-  ( ph  ->  ( th  <->  ta )
)
3 biidd 237 . 2  |-  ( ph  ->  ( et  <->  et )
)
41, 2, 33anbi123d 1299 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  et )
) )
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:  3anbi1d  1303  3anbi2d  1304  f1dom3el3dif  6164  fseq1m1p1  11753  hash2prd  12484  imasdsval  14770  iscatd2  14936  ispos  15434  psgnunilem1  16324  rngpropd  17031  mdetunilem3  18911  mdetunilem9  18917  dvfsumlem2  22191  istrkge  23610  axtg5seg  23618  axtgeucl  23626  axlowdim  23968  axeuclid  23970  eengtrkge  23993  lt2addrd  27259  xlt2addrd  27274  sigaval  27778  issgon  27791  brafs  28220  dfrtrcl2  28574  brofs  29260  funtransport  29286  fvtransport  29287  brifs  29298  ifscgr  29299  brcgr3  29301  cgr3permute3  29302  brfs  29334  btwnconn1lem11  29352  funray  29395  fvray  29396  funline  29397  fvline  29399  rmydioph  30588  usgvad2edg  31906  lpolsetN  36297
  Copyright terms: Public domain W3C validator