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

Theorem 3anbi1d 1443
 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 252 . 2 (𝜑 → (𝜃𝜃))
31, 23anbi12d 1440 1 (𝜑 → ((𝜓𝜃𝜏) ↔ (𝜒𝜃𝜏)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1054 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 197  df-an 385  df-3an 1056 This theorem is referenced by:  vtocl3gaf  3306  axdc4uz  12823  wrdl3s3  13751  relexpindlem  13847  sqrtval  14021  sqreu  14144  coprmprod  15422  mreexexd  16355  mreexexdOLD  16356  iscatd2  16389  lmodprop2d  18973  neiptopnei  20984  hausnei  21180  isreg2  21229  regr1lem2  21591  ustval  22053  ustuqtop4  22095  axtgupdim2  25415  axtgeucl  25416  iscgra  25746  brbtwn  25824  ax5seg  25863  axlowdim  25886  axeuclidlem  25887  wlkonprop  26610  upgr2wlk  26620  upgrf1istrl  26656  elwspths2spth  26934  clwlkclwwlk  26968  clwwlknonel  27070  upgr4cycl4dv4e  27163  extwwlkfab  27342  nvi  27597  br8d  29548  xlt2addrd  29651  isslmd  29883  slmdlema  29884  tgoldbachgt  30869  axtgupdim2OLD  30874  br8  31772  br6  31773  br4  31774  fvtransport  32264  brcolinear2  32290  colineardim1  32293  fscgr  32312  idinside  32316  brsegle  32340  poimirlem28  33567  caures  33686  iscringd  33927  oposlem  34787  cdleme18d  35900  jm2.27  37892  9gbo  41987  11gbo  41988
 Copyright terms: Public domain W3C validator