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

Theorem 3anbi2d 1438
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 1434 1 (𝜑 → ((𝜃𝜓𝜏) ↔ (𝜃𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1084
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 395  df-3an 1086
This theorem is referenced by:  vtocl3gafOLD  3563  vtocl3gaOLD  3565  offval22  8102  ereq2  8742  brttrcl  9756  ttrclss  9763  ttrclselem2  9769  wrdl3s3  14971  mhmlem  19056  isdrngrd  20744  isdrngrdOLD  20746  lmodlema  20841  mdetunilem9  22613  neiptoptop  23126  neiptopnei  23127  hausnei  23323  regr1lem2  23735  ustuqtop4  24240  utopsnneiplem  24243  axtg5seg  28392  axtgupdim2  28398  axtgeucl  28399  brbtwn  28833  axlowdim  28895  axeuclidlem  28896  incistruhgr  29015  issubgr2  29208  wwlksnwwlksnon  29849  upgr4cycl4dv4e  30118  isnvlem  30543  csmdsymi  32267  br8d  32530  slmdlema  33067  constrconj  33603  carsgmon  34148  sitgclg  34176  tgoldbachgt  34509  axtgupdim2ALTV  34514  bnj852  34766  bnj18eq1  34772  bnj938  34782  bnj983  34796  bnj1318  34870  bnj1326  34871  cvmlift3lem4  35150  cvmlift3  35156  br8  35578  br6  35579  br4  35580  brcolinear2  35882  colineardim1  35885  brfs  35903  fscgr  35904  btwnconn1lem7  35917  brsegle  35932  unblimceq0  36210  sdclem2  37443  sdclem1  37444  sdc  37445  fdc  37446  cdleme18d  39994  cdlemk35s  40636  cdlemk39s  40638  monotoddzz  42601  jm2.27  42666  mendlmod  42854  minregex2  43202  fiiuncl  44666  wessf1ornlem  44792  fmulcl  45202  fmuldfeqlem1  45203  fprodcncf  45521  dvmptfprodlem  45565  dvmptfprod  45566  dvnprodlem2  45568  stoweidlem6  45627  stoweidlem8  45629  stoweidlem31  45652  stoweidlem34  45655  stoweidlem43  45664  stoweidlem52  45673  fourierdlem41  45769  fourierdlem48  45775  fourierdlem49  45776  ovnsubaddlem1  46191  ichexmpl2  47042  9gbo  47346  11gbo  47347  lmod1  47875
  Copyright terms: Public domain W3C validator