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

Theorem 3orbi123d 1290
 Description: Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)
Hypotheses
Ref Expression
bi3d.1
bi3d.2
bi3d.3
Assertion
Ref Expression
3orbi123d

Proof of Theorem 3orbi123d
StepHypRef Expression
1 bi3d.1 . . . 4
2 bi3d.2 . . . 4
31, 2orbi12d 783 . . 3
4 bi3d.3 . . 3
53, 4orbi12d 783 . 2
6 df-3or 964 . 2
7 df-3or 964 . 2
85, 6, 73bitr4g 222 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104   wo 698   w3o 962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699 This theorem depends on definitions:  df-bi 116  df-3or 964 This theorem is referenced by:  ordtriexmid  4474  ontriexmidim  4475  wetriext  4530  nntri3or  6429  tridc  6833  exmidontriimlem3  7137  exmidontriimlem4  7138  exmidontriim  7139  onntri35  7151  ltsopi  7219  pitri3or  7221  nqtri3or  7295  elz  9148  ztri3or  9189  qtri3or  10120  trilpo  13563  trirec0  13564  reap0  13578
 Copyright terms: Public domain W3C validator