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

Theorem 3anbi3d 1354
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 245 . 2  |-  ( ph  ->  ( th  <->  th )
)
2 3anbi1d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 23anbi13d 1350 1  |-  ( ph  ->  ( ( th  /\  ta  /\  ps )  <->  ( th  /\  ta  /\  ch )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  ceqsex3v  3099  ceqsex4v  3100  ceqsex8v  3102  vtocl3gaf  3127  mob  3231  offval22  6898  smogt  7111  cfsmolem  8725  fseq1m1p1  11897  2swrd1eqwrdeq  12846  2swrd2eqwrdeq  13076  prodmo  14038  fprod  14043  divalg  14432  funcres2b  15850  posi  16243  mhmlem  16854  isdrngrd  18049  lmodlema  18144  connsub  20484  lmmbr3  22278  lmmcvg  22279  dvmptfsum  22975  axtg5seg  24561  axtgupdim2  24567  axtgeucl  24568  ishlg  24695  hlcomb  24696  brbtwn  24977  axlowdim  25039  axeuclidlem  25040  1pthoncl  25370  3v3e3cycl1  25420  el2wlkonot  25645  el2spthonot  25646  el2spthonot0  25647  usg2wlkonot  25659  rusgra0edg  25731  2spotdisj  25837  nvi  26281  isslmd  28566  slmdlema  28567  inelsros  29048  diffiunisros  29049  axtgupdim2OLD  29533  afsval  29536  brafs  29537  bnj981  29809  bnj1326  29883  cvmlift3lem2  30091  cvmlift3lem4  30093  cvmlift3  30099  frrlem1  30562  brofs  30820  brifs  30858  cgr3permute1  30863  brcolinear2  30873  colineardim1  30876  brfs  30894  btwnconn1  30916  brsegle  30923  rdgeqoa  31817  iscringd  32276  oposlem  32792  ishlat1  32962  3dim1lem5  33075  lvoli2  33190  cdlemk42  34552  diclspsn  34806  monotoddzz  35835  jm2.27  35907  mendlmod  36103  fiiuncl  37443  wessf1ornlem  37496  fmulcl  37696  fmuldfeqlem1  37697  fmuldfeq  37698  fprodcncf  37816  dvnmptdivc  37850  dvnprodlem2  37859  dvnprodlem3  37860  stoweidlem6  37903  stoweidlem8  37905  stoweidlem26  37923  stoweidlem31  37929  stoweidlem62  37960  stoweidlem62OLD  37961  fourierdlem41  38048  fourierdlem48  38055  fourierdlem49  38056  sge0iunmpt  38297  ovnsubaddlem1  38429  isgbe  38889  9gboa  38912  11gboa  38913  bgoldbst  38916  sgoldbaltlem1  38917  sgoldbaltlem2  38918  bgoldbtbndlem4  38940  bgoldbtbnd  38941  pfxsuff1eqwrdeq  38987  usgr2wlkspth  39790  upgr3v3e3cycl  39920  upgr4cycl4dv4e  39925  usgra2pth0  39941
  Copyright terms: Public domain W3C validator