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

Theorem 3anbi12d 1255
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 229 . 2  |-  ( ph  ->  ( et  <->  et )
)
41, 2, 33anbi123d 1254 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  et )  <->  ( ch  /\ 
ta  /\  et )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  3anbi1d  1258  3anbi2d  1259  fseq1m1p1  11123  imasdsval  13741  iscatd2  13906  ispos  14404  rngpropd  15695  dvfsumlem2  19911  lt2addrd  24115  xlt2addrd  24124  sigaval  24493  issgon  24506  dfrtrcl2  25148  axlowdim  25900  axeuclid  25902  brofs  25939  funtransport  25965  fvtransport  25966  brifs  25977  ifscgr  25978  brcgr3  25980  cgr3permute3  25981  brfs  26013  btwnconn1lem11  26031  funray  26074  fvray  26075  funline  26076  fvline  26078  rmydioph  27085  psgnunilem1  27393  cshweqdif2  28270  lpolsetN  32280
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator