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

Theorem 3anbi2d 1442
Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
3anbi2d (𝜑 → ((𝜃𝜓𝜏) ↔ (𝜃𝜒𝜏)))

Proof of Theorem 3anbi2d
StepHypRef Expression
1 biidd 262 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 23anbi12d 1438 1 (𝜑 → ((𝜃𝜓𝜏) ↔ (𝜃𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  vtocl3gaf  3536  vtocl3ga  3537  offval22  8021  ereq2  8659  brttrcl  9654  ttrclss  9661  ttrclselem2  9667  wrdl3s3  14857  mhmlem  18872  isdrngrd  20227  isdrngrdOLD  20229  lmodlema  20341  mdetunilem9  21985  neiptoptop  22498  neiptopnei  22499  hausnei  22695  regr1lem2  23107  ustuqtop4  23612  utopsnneiplem  23615  axtg5seg  27449  axtgupdim2  27455  axtgeucl  27456  brbtwn  27890  axlowdim  27952  axeuclidlem  27953  incistruhgr  28072  issubgr2  28262  wwlksnwwlksnon  28902  upgr4cycl4dv4e  29171  isnvlem  29594  csmdsymi  31318  br8d  31575  slmdlema  32087  carsgmon  32971  sitgclg  32999  tgoldbachgt  33333  axtgupdim2ALTV  33338  bnj852  33590  bnj18eq1  33596  bnj938  33606  bnj983  33620  bnj1318  33694  bnj1326  33695  cvmlift3lem4  33973  cvmlift3  33979  br8  34385  br6  34386  br4  34387  brcolinear2  34689  colineardim1  34692  brfs  34710  fscgr  34711  btwnconn1lem7  34724  brsegle  34739  unblimceq0  35016  sdclem2  36247  sdclem1  36248  sdc  36249  fdc  36250  cdleme18d  38804  cdlemk35s  39446  cdlemk39s  39448  monotoddzz  41310  jm2.27  41375  mendlmod  41563  minregex2  41895  fiiuncl  43361  wessf1ornlem  43491  fmulcl  43908  fmuldfeqlem1  43909  fprodcncf  44227  dvmptfprodlem  44271  dvmptfprod  44272  dvnprodlem2  44274  stoweidlem6  44333  stoweidlem8  44335  stoweidlem31  44358  stoweidlem34  44361  stoweidlem43  44370  stoweidlem52  44379  fourierdlem41  44475  fourierdlem48  44481  fourierdlem49  44482  ovnsubaddlem1  44897  ichexmpl2  45748  9gbo  46052  11gbo  46053  lmod1  46659
  Copyright terms: Public domain W3C validator