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

Theorem 3anbi1d 1400
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 1397 1 (𝜑 → ((𝜓𝜃𝜏) ↔ (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  vtocl3gaf  3265  axdc4uz  12739  wrdl3s3  13655  relexpindlem  13753  sqrtval  13927  sqreu  14050  coprmprod  15318  mreexexd  16248  mreexexdOLD  16249  iscatd2  16282  lmodprop2d  18865  neiptopnei  20876  hausnei  21072  isreg2  21121  regr1lem2  21483  ustval  21946  ustuqtop4  21988  axtgupdim2  25304  axtgeucl  25305  iscgra  25635  brbtwn  25713  ax5seg  25752  axlowdim  25775  axeuclidlem  25776  wlkonprop  26457  upgr2wlk  26467  upgrf1istrl  26503  elwspths2spth  26763  clwlkclwwlk  26804  upgr4cycl4dv4e  26945  extwwlkfab  27112  nvi  27357  br8d  29306  xlt2addrd  29408  isslmd  29582  slmdlema  29583  axtgupdim2OLD  30506  br8  31407  br6  31408  br4  31409  fvtransport  31834  brcolinear2  31860  colineardim1  31863  fscgr  31882  idinside  31886  brsegle  31910  poimirlem28  33108  caures  33227  iscringd  33468  oposlem  33988  cdleme18d  35101  jm2.27  37094  9gboa  40987  11gboa  40988
  Copyright terms: Public domain W3C validator