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

Theorem 3anbi3d 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
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 1299 1  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 971
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 973
This theorem is referenced by:  ceqsex3v  3146  ceqsex4v  3147  ceqsex8v  3149  vtocl3gaf  3173  mob  3278  offval22  6852  smogt  7030  cfsmolem  8641  fseq1m1p1  11757  2swrd1eqwrdeq  12673  2swrd2eqwrdeq  12885  prodmo  13828  fprod  13833  divalg  14148  funcres2b  15388  posi  15781  mhmlem  16392  isdrngrd  17620  lmodlema  17715  connsub  20091  lmmbr3  21868  lmmcvg  21869  dvmptfsum  22545  axtg5seg  24063  axtgupdim2  24070  axtgeucl  24071  hlcomb  24191  iscgra  24373  brbtwn  24407  axlowdim  24469  axeuclidlem  24470  1pthoncl  24799  3v3e3cycl1  24849  el2wlkonot  25074  el2spthonot  25075  el2spthonot0  25076  usg2wlkonot  25088  rusgra0edg  25160  2spotdisj  25266  nvi  25708  isslmd  27982  slmdlema  27983  afsval  28818  brafs  28819  cvmlift3lem2  29032  cvmlift3lem4  29034  cvmlift3  29040  frrlem1  29630  brofs  29886  brifs  29924  cgr3permute1  29929  brcolinear2  29939  colineardim1  29942  brfs  29960  btwnconn1  29982  brsegle  29989  iscringd  30639  monotoddzz  31121  jm2.27  31192  mendlmod  31386  fmulcl  31817  fmuldfeqlem1  31818  fmuldfeq  31819  fprodcncf  31946  dvnmptdivc  31977  dvnprodlem2  31986  dvnprodlem3  31987  stoweidlem6  32030  stoweidlem8  32032  stoweidlem26  32050  stoweidlem31  32055  stoweidlem62  32086  fourierdlem41  32172  fourierdlem48  32179  fourierdlem49  32180  pfxsuff1eqwrdeq  32654  usgra2pth0  32746  bnj981  34428  bnj1326  34502  oposlem  35323  ishlat1  35493  3dim1lem5  35606  lvoli2  35721  cdlemk42  37083  diclspsn  37337
  Copyright terms: Public domain W3C validator