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

Theorem 3anbi1d 1293
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 237 . 2  |-  ( ph  ->  ( th  <->  th )
)
31, 23anbi12d 1290 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  ta )  <->  ( ch  /\ 
th  /\  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  3038  axdc4uz  11804  sqrval  12725  sqreu  12847  mreexexd  14585  iscatd2  14618  lmodprop2d  17006  neiptopnei  18735  hausnei  18931  isreg2  18980  regr1lem2  19312  ustval  19776  ustuqtop4  19818  axtgupdim2  22931  axtgeucl  22932  brbtwn  23144  ax5seg  23183  axlowdim  23206  axeuclidlem  23207  wlkon  23428  wlkonprop  23430  istrl2  23436  is2wlk  23463  pths  23464  nvi  23991  br8d  25941  xlt2addrd  26050  isslmd  26217  slmdlema  26218  relexpindlem  27340  br8  27565  br6  27566  br4  27567  fvtransport  28062  brcolinear2  28088  colineardim1  28091  fscgr  28110  idinside  28114  brsegle  28138  caures  28654  iscringd  28797  jm2.27  29355  is2wlkonot  30380  is2spthonot  30381  el2wlkonot  30386  el2spthonot  30387  el2spthonot0  30388  2wlkonot3v  30392  2spthonot3v  30393  extwwlkfab  30681  oposlem  32825  cdleme18d  33937
  Copyright terms: Public domain W3C validator