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

Theorem 3anbi2d 1306
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1d.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
3anbi2d  |-  ( ph  ->  ( ( th  /\  ps  /\  ta )  <->  ( th  /\  ch  /\  ta )
) )

Proof of Theorem 3anbi2d
StepHypRef Expression
1 biidd 237 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi12d 1302 1  |-  ( ph  ->  ( ( th  /\  ps  /\  ta )  <->  ( th  /\  ch  /\  ta )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 974
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 976
This theorem is referenced by:  vtocl3gaf  3126  offval22  6863  ereq2  7356  mhmlem  16514  isdrngrd  17742  lmodlema  17837  mdetunilem9  19414  neiptoptop  19925  neiptopnei  19926  hausnei  20122  regr1lem2  20533  ustuqtop4  21039  utopsnneiplem  21042  axtg5seg  24241  axtgupdim2  24247  axtgeucl  24248  brbtwn  24619  axlowdim  24681  axeuclidlem  24682  usgra2wlkspthlem1  25036  usgra2wlkspthlem2  25037  el2wlkonot  25286  el2spthonot  25287  el2spthonot0  25288  isnvlem  25917  csmdsymi  27666  br8d  27900  slmdlema  28198  carsgmon  28762  sitgclg  28790  axtgupdim2OLD  29059  bnj852  29306  bnj18eq1  29312  bnj938  29322  bnj983  29336  bnj1318  29408  bnj1326  29409  cvmlift3lem4  29619  cvmlift3  29625  br8  29969  br6  29970  br4  29971  brcolinear2  30396  colineardim1  30399  brfs  30417  fscgr  30418  btwnconn1lem7  30431  brsegle  30446  sdclem2  31517  sdclem1  31518  sdc  31519  fdc  31520  cdleme18d  33313  cdlemk35s  33956  cdlemk39s  33958  monotoddzz  35240  jm2.27  35312  mendlmod  35506  fmulcl  36943  fmuldfeqlem1  36944  fprodcncf  37072  dvmptfprodlem  37109  dvmptfprod  37110  dvnprodlem2  37112  stoweidlem6  37156  stoweidlem8  37158  stoweidlem31  37181  stoweidlem34  37184  stoweidlem43  37193  stoweidlem52  37202  fourierdlem41  37298  fourierdlem48  37305  fourierdlem49  37306  9gboa  37828  11gboa  37829  lmod1  38604
  Copyright terms: Public domain W3C validator