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

Theorem 3anbi2d 1294
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 1290 1  |-  ( ph  ->  ( ( th  /\  ps  /\  ta )  <->  ( th  /\  ch  /\  ta )
) )
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:  vtocl3gaf  3034  offval22  6647  ereq2  7101  isdrngrd  16836  lmodlema  16931  mdetunilem9  18401  neiptoptop  18710  neiptopnei  18711  hausnei  18907  regr1lem2  19288  ustuqtop4  19794  utopsnneiplem  19797  axtg5seg  22901  axtgupdim2  22907  axtgeucl  22908  brbtwn  23096  axlowdim  23158  axeuclidlem  23159  isnvlem  23939  csmdsymi  25689  br8d  25893  slmdlema  26170  sitgclg  26680  cvmlift3lem4  27163  cvmlift3  27169  br8  27517  br6  27518  br4  27519  brcolinear2  28040  colineardim1  28043  brfs  28061  fscgr  28062  btwnconn1lem7  28075  brsegle  28090  sdclem2  28591  sdclem1  28592  sdc  28593  fdc  28594  monotoddzz  29237  jm2.27  29310  mendlmod  29503  fmulcl  29715  fmuldfeqlem1  29716  stoweidlem6  29754  stoweidlem8  29756  stoweidlem31  29779  stoweidlem34  29782  stoweidlem43  29791  stoweidlem52  29800  usgra2wlkspthlem1  30249  usgra2wlkspthlem2  30250  el2wlkonot  30341  el2spthonot  30342  el2spthonot0  30343  lmod1  30923  bnj852  31801  bnj18eq1  31807  bnj938  31817  bnj983  31831  bnj1318  31903  bnj1326  31904  cdleme18d  33779  cdlemk35s  34421  cdlemk39s  34423
  Copyright terms: Public domain W3C validator