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

Theorem 3anbi2d 1441
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
3anbi2d (𝜑 → ((𝜃𝜓𝜏) ↔ (𝜃𝜒𝜏)))

Proof of Theorem 3anbi2d
StepHypRef Expression
1 biidd 261 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 23anbi12d 1437 1 (𝜑 → ((𝜃𝜓𝜏) ↔ (𝜃𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  vtocl3gaf  3538  vtocl3ga  3539  offval22  8025  ereq2  8663  brttrcl  9658  ttrclss  9665  ttrclselem2  9671  wrdl3s3  14863  mhmlem  18881  isdrngrd  20256  isdrngrdOLD  20258  lmodlema  20383  mdetunilem9  22006  neiptoptop  22519  neiptopnei  22520  hausnei  22716  regr1lem2  23128  ustuqtop4  23633  utopsnneiplem  23636  axtg5seg  27470  axtgupdim2  27476  axtgeucl  27477  brbtwn  27911  axlowdim  27973  axeuclidlem  27974  incistruhgr  28093  issubgr2  28283  wwlksnwwlksnon  28923  upgr4cycl4dv4e  29192  isnvlem  29615  csmdsymi  31339  br8d  31596  slmdlema  32108  carsgmon  33003  sitgclg  33031  tgoldbachgt  33365  axtgupdim2ALTV  33370  bnj852  33622  bnj18eq1  33628  bnj938  33638  bnj983  33652  bnj1318  33726  bnj1326  33727  cvmlift3lem4  34003  cvmlift3  34009  br8  34415  br6  34416  br4  34417  brcolinear2  34719  colineardim1  34722  brfs  34740  fscgr  34741  btwnconn1lem7  34754  brsegle  34769  unblimceq0  35046  sdclem2  36274  sdclem1  36275  sdc  36276  fdc  36277  cdleme18d  38831  cdlemk35s  39473  cdlemk39s  39475  monotoddzz  41325  jm2.27  41390  mendlmod  41578  minregex2  41929  fiiuncl  43395  wessf1ornlem  43525  fmulcl  43942  fmuldfeqlem1  43943  fprodcncf  44261  dvmptfprodlem  44305  dvmptfprod  44306  dvnprodlem2  44308  stoweidlem6  44367  stoweidlem8  44369  stoweidlem31  44392  stoweidlem34  44395  stoweidlem43  44404  stoweidlem52  44413  fourierdlem41  44509  fourierdlem48  44515  fourierdlem49  44516  ovnsubaddlem1  44931  ichexmpl2  45782  9gbo  46086  11gbo  46087  lmod1  46693
  Copyright terms: Public domain W3C validator