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

Theorem 3anbi123d 1244
 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 457 . . 3
4 bi3d.3 . . 3
53, 4anbi12d 457 . 2
6 df-3an 922 . 2
7 df-3an 922 . 2
85, 6, 73bitr4g 221 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 102   wb 103   w3a 920 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106 This theorem depends on definitions:  df-bi 115  df-3an 922 This theorem is referenced by:  3anbi12d  1245  3anbi13d  1246  3anbi23d  1247  limeq  4140  smoeq  5939  tfrlemi1  5981  tfr1onlemaccex  5997  tfrcllemaccex  6010  ereq1  6179  elinp  6726  iccshftr  9092  iccshftl  9094  iccdil  9096  icccntr  9098  fzaddel  9153  elfzomelpfzo  9317  sumeq1  10330  divalglemnn  10462  divalglemeunn  10465  divalglemeuneg  10467  dfgcd2  10547
 Copyright terms: Public domain W3C validator