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

Theorem 3anbi2d 1260
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 230 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi12d 1256 1  |-  ( ph  ->  ( ( th  /\  ps  /\  ta )  <->  ( th  /\  ch  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ w3a 937
This theorem is referenced by:  vtocl3gaf  3022  ereq2  6915  isdrngrd  15863  lmodlema  15957  neiptoptop  17197  neiptopnei  17198  hausnei  17394  regr1lem2  17774  ustuqtop4  18276  utopsnneiplem  18279  isnvlem  22091  csmdsymi  23839  sitgclg  24658  cvmlift3lem4  25011  cvmlift3  25017  br8  25381  br6  25382  br4  25383  brbtwn  25840  axlowdim  25902  axeuclidlem  25903  brcolinear2  25994  colineardim1  25997  brfs  26015  fscgr  26016  btwnconn1lem7  26029  brsegle  26044  sdclem2  26448  sdclem1  26449  sdc  26450  fdc  26451  monotoddzz  27008  jm2.27  27081  mendlmod  27480  fmulcl  27689  fmuldfeqlem1  27690  stoweidlem6  27733  stoweidlem8  27735  stoweidlem31  27758  stoweidlem34  27761  stoweidlem43  27770  stoweidlem52  27779  usgra2wlkspthlem1  28308  usgra2wlkspthlem2  28309  el2wlkonot  28338  el2spthonot  28339  el2spthonot0  28340  bnj852  29294  bnj18eq1  29300  bnj938  29310  bnj983  29324  bnj1318  29396  bnj1326  29397  cdleme18d  31094  cdlemk35s  31736  cdlemk39s  31738
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator