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

Theorem 3anbi1d 1440
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 1437 1 (𝜑 → ((𝜓𝜃𝜏) ↔ (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  vtocl3gaf  3537  vtocl3ga  3538  axdc4uz  13888  wrdl3s3  14850  relexpindlem  14947  sqrtval  15121  sqreu  15244  coprmprod  16536  mreexexd  17527  iscatd2  17560  lmodprop2d  20382  neiptopnei  22481  hausnei  22677  isreg2  22726  regr1lem2  23089  ustval  23552  ustuqtop4  23594  axtgupdim2  27411  axtgeucl  27412  iscgra  27749  brbtwn  27846  ax5seg  27885  axlowdim  27908  axeuclidlem  27909  wlkonprop  28604  upgr2wlk  28614  upgrf1istrl  28649  elwspths2spth  28910  clwlkclwwlk  28944  clwwlknonel  29037  upgr4cycl4dv4e  29127  extwwlkfab  29294  nvi  29554  br8d  31527  xlt2addrd  31658  isslmd  32032  slmdlema  32033  tgoldbachgt  33267  axtgupdim2ALTV  33272  br8  34320  br6  34321  br4  34322  fvtransport  34608  brcolinear2  34634  colineardim1  34637  fscgr  34656  idinside  34660  brsegle  34684  poimirlem28  36097  caures  36210  iscringd  36448  oposlem  37635  cdleme18d  38749  jm2.27  41310  ichexmpl2  45634  ichnreuop  45636  9gbo  45938  11gbo  45939
  Copyright terms: Public domain W3C validator