MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi12d Unicode version

Theorem 3anbi12d 1300
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
Hypotheses
Ref Expression
3anbi12d.1
3anbi12d.2
Assertion
Ref Expression
3anbi12d

Proof of Theorem 3anbi12d
StepHypRef Expression
1 3anbi12d.1 . 2
2 3anbi12d.2 . 2
3 biidd 237 . 2
41, 2, 33anbi123d 1299 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\w3a 973
This theorem is referenced by:  3anbi1d  1303  3anbi2d  1304  f1dom3el3dif  6176  fseq1m1p1  11782  hash2prd  12518  imasdsval  14912  iscatd2  15078  ispos  15576  psgnunilem1  16518  ringpropd  17230  mdetunilem3  19116  mdetunilem9  19122  dvfsumlem2  22428  istrkge  23854  axtg5seg  23862  axtgeucl  23870  axlowdim  24264  axeuclid  24266  eengtrkge  24289  lt2addrd  27563  xlt2addrd  27578  sigaval  28110  issgon  28123  brafs  28552  dfrtrcl2  29071  brofs  29655  funtransport  29681  fvtransport  29682  brifs  29693  ifscgr  29694  brcgr3  29696  cgr3permute3  29697  brfs  29729  btwnconn1lem11  29747  funray  29790  fvray  29791  funline  29792  fvline  29794  rmydioph  30956  usgvad2edg  32411  lpolsetN  37209
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator