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

Theorem 3anbi1d 1434
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 264 . 2 (𝜑 → (𝜃𝜃))
31, 23anbi12d 1431 1 (𝜑 → ((𝜓𝜃𝜏) ↔ (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  w3a 1082
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 209  df-an 399  df-3an 1084
This theorem is referenced by:  vtocl3gaf  3575  axdc4uz  13344  wrdl3s3  14318  relexpindlem  14414  sqrtval  14588  sqreu  14712  coprmprod  15997  mreexexd  16911  iscatd2  16944  lmodprop2d  19688  neiptopnei  21732  hausnei  21928  isreg2  21977  regr1lem2  22340  ustval  22803  ustuqtop4  22845  axtgupdim2  26249  axtgeucl  26250  iscgra  26587  brbtwn  26677  ax5seg  26716  axlowdim  26739  axeuclidlem  26740  wlkonprop  27432  upgr2wlk  27442  upgrf1istrl  27477  elwspths2spth  27738  clwlkclwwlk  27772  clwwlknonel  27866  upgr4cycl4dv4e  27956  extwwlkfab  28123  nvi  28383  br8d  30353  xlt2addrd  30474  isslmd  30823  slmdlema  30824  tgoldbachgt  31927  axtgupdim2ALTV  31932  br8  32985  br6  32986  br4  32987  fvtransport  33486  brcolinear2  33512  colineardim1  33515  fscgr  33534  idinside  33538  brsegle  33562  poimirlem28  34912  caures  35027  iscringd  35268  oposlem  36310  cdleme18d  37423  jm2.27  39595  ichexmpl2  43622  ichnreuop  43624  9gbo  43929  11gbo  43930
  Copyright terms: Public domain W3C validator