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

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

Proof of Theorem 3anbi1d
StepHypRef Expression
1 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 biidd 228 . 2  |-  ( ph  ->  ( th  <->  th )
)
31, 23anbi12d 1253 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  ta )  <->  ( ch  /\ 
th  /\  ta )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  vtocl3gaf  2865  axdc4uz  11061  sqrval  11738  sqreu  11860  mreexexd  13566  iscatd2  13599  lmodprop2d  15703  hausnei  17072  isreg2  17121  regr1lem2  17447  nvi  21186  xlt2addrd  23268  relexpindlem  24051  br8  24184  br6  24185  br4  24186  brbtwn  24599  ax5seg  24638  axlowdim  24661  axeuclidlem  24662  fvtransport  24727  brcolinear2  24753  colineardim1  24756  fscgr  24775  idinside  24779  brsegle  24803  tpssg  25035  isibg2  26213  isibg2aa  26215  isibg2aalem1  26216  caures  26579  iscringd  26727  jm2.27  27204  iswlkon  28332  istrl2  28337  pths  28352  oposlem  29995  cdleme18d  31106
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