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

Theorem 3anbi1d 1303
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 1300 1  |-  ( ph  ->  ( ( ps  /\  th 
/\  ta )  <->  ( ch  /\ 
th  /\  ta )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 972
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 369  df-3an 974
This theorem is referenced by:  vtocl3gaf  3123  axdc4uz  12045  relexpindlem  12950  sqrtval  13124  sqreu  13247  mreexexd  15152  iscatd2  15185  lmodprop2d  17782  neiptopnei  19816  hausnei  20012  isreg2  20061  regr1lem2  20423  ustval  20887  ustuqtop4  20929  axtgupdim2OLD  24141  axtgupdim2  24142  axtgeucl  24143  iscgra  24449  brbtwn  24501  ax5seg  24540  axlowdim  24563  axeuclidlem  24564  wlkon  24832  wlkonprop  24834  istrl2  24839  is2wlk  24866  pths  24867  is2wlkonot  25162  is2spthonot  25163  el2wlkonot  25168  el2spthonot  25169  el2spthonot0  25170  2wlkonot3v  25174  2spthonot3v  25175  extwwlkfab  25389  nvi  25802  br8d  27781  xlt2addrd  27901  isslmd  28078  slmdlema  28079  br8  29850  br6  29851  br4  29852  fvtransport  30338  brcolinear2  30364  colineardim1  30367  fscgr  30386  idinside  30390  brsegle  30414  caures  31499  iscringd  31642  oposlem  32164  cdleme18d  33277  jm2.27  35276
  Copyright terms: Public domain W3C validator