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

Theorem 3anbi3d 1296
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 1292 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  3118  ceqsex4v  3119  ceqsex8v  3121  vtocl3gaf  3145  mob  3248  offval22  6765  smogt  6941  cfsmolem  8553  fseq1m1p1  11655  2swrd1eqwrdeq  12469  2swrd2eqwrdeq  12674  divalg  13728  funcres2b  14929  posi  15242  isdrngrd  16984  lmodlema  17079  connsub  19160  lmmbr3  20906  lmmcvg  20907  dvmptfsum  21583  axtg5seg  23062  axtgupdim2  23069  axtgeucl  23070  brbtwn  23317  axlowdim  23379  axeuclidlem  23380  1pthoncl  23663  3v3e3cycl1  23702  nvi  24164  isslmd  26383  slmdlema  26384  afsval  27159  brafs  27160  cvmlift3lem2  27373  cvmlift3lem4  27375  cvmlift3  27381  prodmo  27613  fprod  27618  frrlem1  27932  brofs  28200  brifs  28238  cgr3permute1  28243  brcolinear2  28253  colineardim1  28256  brfs  28274  btwnconn1  28296  brsegle  28303  iscringd  28967  monotoddzz  29452  jm2.27  29525  mendlmod  29718  fmulcl  29930  fmuldfeqlem1  29931  fmuldfeq  29932  stoweidlem6  29969  stoweidlem8  29971  stoweidlem26  29989  stoweidlem31  29994  stoweidlem62  30025  usgra2pth0  30470  el2wlkonot  30556  el2spthonot  30557  el2spthonot0  30558  usg2wlkonot  30570  rusgra0edg  30741  2spotdisj  30822  bnj981  32295  bnj1326  32369  oposlem  33185  ishlat1  33355  3dim1lem5  33468  lvoli2  33583  cdlemk42  34943  diclspsn  35197
  Copyright terms: Public domain W3C validator