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

Theorem 3anbi12d 1298
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 1297 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  et )
) )
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:  3anbi1d  1301  3anbi2d  1302  f1dom3el3dif  6151  fseq1m1p1  11757  hash2prd  12505  dfrtrcl2  12980  imasdsval  15007  iscatd2  15173  ispos  15778  psgnunilem1  16720  ringpropd  17428  mdetunilem3  19286  mdetunilem9  19292  dvfsumlem2  22597  istrkge  24055  axtg5seg  24063  axtgeucl  24071  cgraid  24374  axlowdim  24469  axeuclid  24471  eengtrkge  24494  lt2addrd  27797  xlt2addrd  27812  sigaval  28343  issgon  28356  brafs  28819  brofs  29886  funtransport  29912  fvtransport  29913  brifs  29924  ifscgr  29925  brcgr3  29927  cgr3permute3  29928  brfs  29960  btwnconn1lem11  29978  funray  30021  fvray  30022  funline  30023  fvline  30025  rmydioph  31198  usgvad2edg  32802  lpolsetN  37625  iunrelexpmin2  38229
  Copyright terms: Public domain W3C validator