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

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

Proof of Theorem 3anbi1d
StepHypRef Expression
1 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
2 biidd 254 . 2 (𝜑 → (𝜃𝜃))
31, 23anbi12d 1567 1 (𝜑 → ((𝜓𝜃𝜏) ↔ (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  w3a 1113
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 199  df-an 387  df-3an 1115
This theorem is referenced by:  vtocl3gaf  3491  axdc4uz  13077  wrdl3s3  14083  relexpindlem  14179  sqrtval  14353  sqreu  14476  coprmprod  15746  mreexexd  16660  iscatd2  16693  lmodprop2d  19280  neiptopnei  21306  hausnei  21502  isreg2  21551  regr1lem2  21913  ustval  22375  ustuqtop4  22417  axtgupdim2  25782  axtgeucl  25783  iscgra  26117  brbtwn  26197  ax5seg  26236  axlowdim  26259  axeuclidlem  26260  wlkonprop  26954  upgr2wlk  26964  upgrf1istrl  27005  elwspths2spth  27295  clwlkclwwlk  27330  clwlkclwwlkOLD  27331  clwwlknonel  27467  upgr4cycl4dv4e  27560  extwwlkfab  27739  extwwlkfabOLD  27740  nvi  28023  br8d  29968  xlt2addrd  30069  isslmd  30299  slmdlema  30300  tgoldbachgt  31289  axtgupdim2OLD  31294  br8  32187  br6  32188  br4  32189  fvtransport  32677  brcolinear2  32703  colineardim1  32706  fscgr  32725  idinside  32729  brsegle  32753  poimirlem28  33980  caures  34097  iscringd  34338  oposlem  35256  cdleme18d  36369  jm2.27  38417  9gbo  42491  11gbo  42492
  Copyright terms: Public domain W3C validator