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

Theorem 3anbi1d 1437
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 261 . 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  axdc4uz  14004  wrdl3s3  14971  relexpindlem  15068  sqrtval  15242  sqreu  15365  coprmprod  16662  mreexexd  17661  iscatd2  17694  lmodprop2d  20900  neiptopnei  23127  hausnei  23323  isreg2  23372  regr1lem2  23735  ustval  24198  ustuqtop4  24240  axtgupdim2  28398  axtgeucl  28399  iscgra  28736  brbtwn  28833  ax5seg  28872  axlowdim  28895  axeuclidlem  28896  wlkonprop  29595  upgr2wlk  29605  upgrf1istrl  29640  elwspths2spth  29901  clwlkclwwlk  29935  clwwlknonel  30028  upgr4cycl4dv4e  30118  extwwlkfab  30285  nvi  30547  br8d  32530  xlt2addrd  32662  isslmd  33066  slmdlema  33067  tgoldbachgt  34509  axtgupdim2ALTV  34514  br8  35578  br6  35579  br4  35580  fvtransport  35856  brcolinear2  35882  colineardim1  35885  fscgr  35904  idinside  35908  brsegle  35932  poimirlem28  37349  caures  37461  iscringd  37699  oposlem  38880  cdleme18d  39994  jm2.27  42666  ichexmpl2  47042  ichnreuop  47044  9gbo  47346  11gbo  47347
  Copyright terms: Public domain W3C validator