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

Theorem 3anbi3d 1305
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 1301 1  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973
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 975
This theorem is referenced by:  ceqsex3v  3158  ceqsex4v  3159  ceqsex8v  3161  vtocl3gaf  3185  mob  3290  offval22  6874  smogt  7050  cfsmolem  8662  fseq1m1p1  11765  2swrd1eqwrdeq  12659  2swrd2eqwrdeq  12871  divalg  13937  funcres2b  15141  posi  15454  mhmlem  16062  isdrngrd  17293  lmodlema  17388  connsub  19790  lmmbr3  21567  lmmcvg  21568  dvmptfsum  22244  axtg5seg  23728  axtgupdim2  23735  axtgeucl  23736  brbtwn  24025  axlowdim  24087  axeuclidlem  24088  1pthoncl  24417  3v3e3cycl1  24467  el2wlkonot  24692  el2spthonot  24693  el2spthonot0  24694  usg2wlkonot  24706  rusgra0edg  24778  2spotdisj  24885  nvi  25330  isslmd  27569  slmdlema  27570  afsval  28376  brafs  28377  cvmlift3lem2  28590  cvmlift3lem4  28592  cvmlift3  28598  prodmo  28995  fprod  29000  frrlem1  29314  brofs  29582  brifs  29620  cgr3permute1  29625  brcolinear2  29635  colineardim1  29638  brfs  29656  btwnconn1  29678  brsegle  29685  iscringd  30323  monotoddzz  30807  jm2.27  30878  mendlmod  31071  fmulcl  31454  fmuldfeqlem1  31455  fmuldfeq  31456  stoweidlem6  31629  stoweidlem8  31631  stoweidlem26  31649  stoweidlem31  31654  stoweidlem62  31685  fourierdlem41  31771  fourierdlem48  31778  fourierdlem49  31779  usgra2pth0  32145  bnj981  33488  bnj1326  33562  oposlem  34380  ishlat1  34550  3dim1lem5  34663  lvoli2  34778  cdlemk42  36138  diclspsn  36392
  Copyright terms: Public domain W3C validator