Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3anbi123d Unicode version

Theorem 3anbi123d 1294
 Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
Hypotheses
Ref Expression
bi3d.1
bi3d.2
bi3d.3
Assertion
Ref Expression
3anbi123d

Proof of Theorem 3anbi123d
StepHypRef Expression
1 bi3d.1 . . . 4
2 bi3d.2 . . . 4
31, 2anbi12d 465 . . 3
4 bi3d.3 . . 3
53, 4anbi12d 465 . 2
6 df-3an 965 . 2
7 df-3an 965 . 2
85, 6, 73bitr4g 222 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   w3a 963 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 965 This theorem is referenced by:  3anbi12d  1295  3anbi13d  1296  3anbi23d  1297  limeq  4336  smoeq  6231  tfrlemi1  6273  tfr1onlemaccex  6289  tfrcllemaccex  6302  ereq1  6480  updjud  7016  ctssdclemr  7046  elinp  7377  sup3exmid  8811  iccshftr  9880  iccshftl  9882  iccdil  9884  icccntr  9886  fzaddel  9943  elfzomelpfzo  10112  seq3f1olemstep  10382  seq3f1olemp  10383  sumeq1  11234  summodclem2  11261  summodc  11262  zsumdc  11263  prodmodclem2  11456  prodmodc  11457  divalglemnn  11790  divalglemeunn  11793  divalglemeuneg  11795  dfgcd2  11878  ctiunct  12141  isstruct2im  12160  isstruct2r  12161  fiinopn  12362  lmfval  12552  upxp  12632  2irrexpqap  13255  dceqnconst  13592  dcapnconst  13593
 Copyright terms: Public domain W3C validator