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

Theorem 3anbi12d 1290
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 1289 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  et )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 965
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 967
This theorem is referenced by:  3anbi1d  1293  3anbi2d  1294  f1dom3el3dif  5979  fseq1m1p1  11533  hash2prd  12179  imasdsval  14451  iscatd2  14617  ispos  15115  psgnunilem1  15997  rngpropd  16674  mdetunilem3  18418  mdetunilem9  18424  dvfsumlem2  21497  istrkge  22918  axtg5seg  22924  axtgeucl  22931  axlowdim  23205  axeuclid  23207  eengtrkge  23230  lt2addrd  26034  xlt2addrd  26049  sigaval  26551  issgon  26564  brafs  26994  dfrtrcl2  27348  brofs  28034  funtransport  28060  fvtransport  28061  brifs  28072  ifscgr  28073  brcgr3  28075  cgr3permute3  28076  brfs  28108  btwnconn1lem11  28126  funray  28169  fvray  28170  funline  28171  fvline  28173  rmydioph  29360  lpolsetN  35124
  Copyright terms: Public domain W3C validator