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

Theorem 3anbi1d 1395
 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 251 . 2 (𝜑 → (𝜃𝜃))
31, 23anbi12d 1392 1 (𝜑 → ((𝜓𝜃𝜏) ↔ (𝜒𝜃𝜏)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  vtocl3gaf  3248  axdc4uz  12645  wrdl3s3  13553  relexpindlem  13651  sqrtval  13825  sqreu  13948  coprmprod  15213  mreexexd  16131  mreexexdOLD  16132  iscatd2  16165  lmodprop2d  18748  neiptopnei  20746  hausnei  20942  isreg2  20991  regr1lem2  21353  ustval  21816  ustuqtop4  21858  axtgupdim2  25170  axtgeucl  25171  iscgra  25501  brbtwn  25579  ax5seg  25618  axlowdim  25641  axeuclidlem  25642  wlkon  26061  wlkonprop  26063  istrl2  26068  is2wlk  26095  pths  26096  is2wlkonot  26390  is2spthonot  26391  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  2wlkonot3v  26402  2spthonot3v  26403  extwwlkfab  26617  nvi  26853  br8d  28802  xlt2addrd  28913  isslmd  29086  slmdlema  29087  axtgupdim2OLD  29999  br8  30899  br6  30900  br4  30901  fvtransport  31309  brcolinear2  31335  colineardim1  31338  fscgr  31357  idinside  31361  brsegle  31385  poimirlem28  32607  caures  32726  iscringd  32967  oposlem  33487  cdleme18d  34600  jm2.27  36593  9gboa  40196  11gboa  40197  wlkOnprop  40866  upgr2wlk  40876  upgrf1istrl  40911  elwspths2spth  41171  clwlkclwwlk  41211  upgr4cycl4dv4e  41352  av-extwwlkfab  41520
 Copyright terms: Public domain W3C validator