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

Theorem 3anbi2d 1401
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 252 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 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  3266  offval22  7199  ereq2  7696  wrdl3s3  13634  mhmlem  17451  isdrngrd  18689  lmodlema  18784  mdetunilem9  20340  neiptoptop  20840  neiptopnei  20841  hausnei  21037  regr1lem2  21448  ustuqtop4  21953  utopsnneiplem  21956  axtg5seg  25259  axtgupdim2  25265  axtgeucl  25266  brbtwn  25674  axlowdim  25736  axeuclidlem  25737  incistruhgr  25865  issubgr2  26051  wwlksnwwlksnon  26673  upgr4cycl4dv4e  26905  isnvlem  27305  csmdsymi  29033  br8d  29256  slmdlema  29533  carsgmon  30149  sitgclg  30177  axtgupdim2OLD  30445  bnj852  30691  bnj18eq1  30697  bnj938  30707  bnj983  30721  bnj1318  30793  bnj1326  30794  cvmlift3lem4  31004  cvmlift3  31010  br8  31346  br6  31347  br4  31348  brcolinear2  31799  colineardim1  31802  brfs  31820  fscgr  31821  btwnconn1lem7  31834  brsegle  31849  unblimceq0  32132  sdclem2  33156  sdclem1  33157  sdc  33158  fdc  33159  cdleme18d  35048  cdlemk35s  35691  cdlemk39s  35693  monotoddzz  36974  jm2.27  37041  mendlmod  37230  fiiuncl  38705  wessf1ornlem  38831  fmulcl  39204  fmuldfeqlem1  39205  fprodcncf  39405  dvmptfprodlem  39452  dvmptfprod  39453  dvnprodlem2  39455  stoweidlem6  39517  stoweidlem8  39519  stoweidlem31  39542  stoweidlem34  39545  stoweidlem43  39554  stoweidlem52  39563  fourierdlem41  39659  fourierdlem48  39665  fourierdlem49  39666  ovnsubaddlem1  40078  9gboa  40945  11gboa  40946  lmod1  41543
  Copyright terms: Public domain W3C validator