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

Theorem 3anbi1d 1394
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 250 . 2 (𝜑 → (𝜃𝜃))
31, 23anbi12d 1391 1 (𝜑 → ((𝜓𝜃𝜏) ↔ (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  vtocl3gaf  3244  axdc4uz  12597  wrdl3s3  13496  relexpindlem  13594  sqrtval  13768  sqreu  13891  coprmprod  15156  mreexexd  16074  mreexexdOLD  16075  iscatd2  16108  lmodprop2d  18691  neiptopnei  20685  hausnei  20881  isreg2  20930  regr1lem2  21292  ustval  21755  ustuqtop4  21797  axtgupdim2  25084  axtgeucl  25085  iscgra  25416  brbtwn  25494  ax5seg  25533  axlowdim  25556  axeuclidlem  25557  wlkon  25824  wlkonprop  25826  istrl2  25831  is2wlk  25858  pths  25859  is2wlkonot  26153  is2spthonot  26154  el2wlkonot  26159  el2spthonot  26160  el2spthonot0  26161  2wlkonot3v  26165  2spthonot3v  26166  extwwlkfab  26380  nvi  26634  br8d  28605  xlt2addrd  28716  isslmd  28889  slmdlema  28890  axtgupdim2OLD  29802  br8  30702  br6  30703  br4  30704  fvtransport  31112  brcolinear2  31138  colineardim1  31141  fscgr  31160  idinside  31164  brsegle  31188  poimirlem28  32407  caures  32526  iscringd  32767  oposlem  33287  cdleme18d  34400  jm2.27  36393  9gboa  39998  11gboa  39999  wlkOnprop  40865  upgr2wlk  40875  upgrf1istrl  40910  elwspths2spth  41170  clwlkclwwlk  41210  upgr4cycl4dv4e  41351  av-extwwlkfab  41519
  Copyright terms: Public domain W3C validator