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  2852  axdc4uz  11045  sqrval  11722  sqreu  11844  mreexexd  13550  iscatd2  13583  lmodprop2d  15687  hausnei  17056  isreg2  17105  regr1lem2  17431  nvi  21170  xlt2addrd  23253  relexpindlem  24036  br8  24113  br6  24114  br4  24115  brbtwn  24527  ax5seg  24566  axlowdim  24589  axeuclidlem  24590  fvtransport  24655  brcolinear2  24681  colineardim1  24684  fscgr  24703  idinside  24707  brsegle  24731  tpssg  24932  isibg2  26110  isibg2aa  26112  isibg2aalem1  26113  caures  26476  iscringd  26624  jm2.27  27101  oposlem  29373  cdleme18d  30484
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