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

Theorem 3anbi123d 1207
 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 442 . . 3
4 bi3d.3 . . 3
53, 4anbi12d 442 . 2
6 df-3an 887 . 2
7 df-3an 887 . 2
85, 6, 73bitr4g 212 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 97   wb 98   w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  3anbi12d  1208  3anbi13d  1209  3anbi23d  1210  sbc3ang  2820  limeq  4114  smoeq  5905  tfrlemi1  5946  ereq1  6113  elinp  6572  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  fzaddel  8922  elfzomelpfzo  9087
 Copyright terms: Public domain W3C validator