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

Theorem 3anbi2d 1433
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 263 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 23anbi12d 1429 1 (𝜑 → ((𝜃𝜓𝜏) ↔ (𝜃𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  w3a 1080
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 208  df-an 397  df-3an 1082
This theorem is referenced by:  vtocl3gaf  3520  offval22  7644  ereq2  8152  wrdl3s3  14165  mhmlem  17981  isdrngrd  19223  lmodlema  19334  mdetunilem9  20918  neiptoptop  21428  neiptopnei  21429  hausnei  21625  regr1lem2  22037  ustuqtop4  22541  utopsnneiplem  22544  axtg5seg  25938  axtgupdim2  25944  axtgeucl  25945  brbtwn  26373  axlowdim  26435  axeuclidlem  26436  incistruhgr  26552  issubgr2  26742  wwlksnwwlksnon  27386  upgr4cycl4dv4e  27656  isnvlem  28083  csmdsymi  29807  br8d  30056  slmdlema  30474  carsgmon  31194  sitgclg  31222  tgoldbachgt  31556  axtgupdim2ALTV  31561  bnj852  31814  bnj18eq1  31820  bnj938  31830  bnj983  31844  bnj1318  31916  bnj1326  31917  cvmlift3lem4  32184  cvmlift3  32190  br8  32607  br6  32608  br4  32609  brcolinear2  33135  colineardim1  33138  brfs  33156  fscgr  33157  btwnconn1lem7  33170  brsegle  33185  unblimceq0  33462  sdclem2  34575  sdclem1  34576  sdc  34577  fdc  34578  cdleme18d  36988  cdlemk35s  37630  cdlemk39s  37632  monotoddzz  39051  jm2.27  39116  mendlmod  39304  fiiuncl  40892  wessf1ornlem  41011  fmulcl  41430  fmuldfeqlem1  41431  fprodcncf  41752  dvmptfprodlem  41797  dvmptfprod  41798  dvnprodlem2  41800  stoweidlem6  41860  stoweidlem8  41862  stoweidlem31  41885  stoweidlem34  41888  stoweidlem43  41897  stoweidlem52  41906  fourierdlem41  42002  fourierdlem48  42008  fourierdlem49  42009  ovnsubaddlem1  42421  ichexmpl2  43141  9gbo  43448  11gbo  43449  lmod1  44054
  Copyright terms: Public domain W3C validator