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

Theorem 3anbi2d 1257
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 228 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi12d 1253 1  |-  ( ph  ->  ( ( th  /\  ps  /\  ta )  <->  ( th  /\  ch  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  vtocl3gaf  2865  ereq2  6684  isdrngrd  15554  lmodlema  15648  hausnei  17072  regr1lem2  17447  isnvlem  21182  csmdsymi  22930  cvmlift3lem4  23868  cvmlift3  23874  br8  24184  br6  24185  br4  24186  brbtwn  24599  axlowdim  24661  axeuclidlem  24662  brcolinear2  24753  colineardim1  24756  brfs  24774  fscgr  24775  btwnconn1lem7  24788  brsegle  24803  tpssg  25035  isalg  25824  algi  25830  iepiclem  25926  rocatval2  26063  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  sdclem2  26555  sdclem1  26556  sdc  26557  fdc  26558  monotoddzz  27131  jm2.27  27204  mendlmod  27604  fmulcl  27814  fmuldfeqlem1  27815  stoweidlem6  27858  stoweidlem8  27860  stoweidlem31  27883  stoweidlem34  27886  stoweidlem43  27895  stoweidlem51  27903  bnj852  29269  bnj18eq1  29275  bnj938  29285  bnj983  29299  bnj1318  29371  bnj1326  29372  cdleme18d  31106  cdlemk35s  31748  cdlemk39s  31750
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator