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

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

Proof of Theorem 3anbi3d
StepHypRef Expression
1 biidd 237 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi13d 1291 1  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )
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:  ceqsex3v  3007  ceqsex4v  3008  ceqsex8v  3010  vtocl3gaf  3034  mob  3136  offval22  6647  smogt  6820  cfsmolem  8431  fseq1m1p1  11527  2swrd1eqwrdeq  12340  2swrd2eqwrdeq  12545  divalg  13599  funcres2b  14799  posi  15112  isdrngrd  16836  lmodlema  16931  connsub  19000  lmmbr3  20746  lmmcvg  20747  dvmptfsum  21422  axtg5seg  22901  axtgupdim2  22907  axtgeucl  22908  brbtwn  23096  axlowdim  23158  axeuclidlem  23159  1pthoncl  23442  3v3e3cycl1  23481  nvi  23943  isslmd  26169  slmdlema  26170  afsval  26947  brafs  26948  cvmlift3lem2  27161  cvmlift3lem4  27163  cvmlift3  27169  prodmo  27400  fprod  27405  frrlem1  27719  brofs  27987  brifs  28025  cgr3permute1  28030  brcolinear2  28040  colineardim1  28043  brfs  28061  btwnconn1  28083  brsegle  28090  iscringd  28752  monotoddzz  29237  jm2.27  29310  mendlmod  29503  fmulcl  29715  fmuldfeqlem1  29716  fmuldfeq  29717  stoweidlem6  29754  stoweidlem8  29756  stoweidlem26  29774  stoweidlem31  29779  stoweidlem62  29810  usgra2pth0  30255  el2wlkonot  30341  el2spthonot  30342  el2spthonot0  30343  usg2wlkonot  30355  rusgra0edg  30526  2spotdisj  30607  bnj981  31830  bnj1326  31904  oposlem  32667  ishlat1  32837  3dim1lem5  32950  lvoli2  33065  cdlemk42  34425  diclspsn  34679
  Copyright terms: Public domain W3C validator