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

Theorem 3orbi123d 1311
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 793 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4orbi12d 793 . 2 (𝜑 → (((𝜓𝜃) ∨ 𝜂) ↔ ((𝜒𝜏) ∨ 𝜁)))
6 df-3or 979 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∨ 𝜂))
7 df-3or 979 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∨ 𝜁))
85, 6, 73bitr4g 223 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wo 708  w3o 977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709
This theorem depends on definitions:  df-bi 117  df-3or 979
This theorem is referenced by:  ordtriexmid  4522  ontriexmidim  4523  wetriext  4578  nntri3or  6496  tridc  6901  exmidontriimlem3  7224  exmidontriimlem4  7225  exmidontriim  7226  onntri35  7238  ltsopi  7321  pitri3or  7323  nqtri3or  7397  elz  9257  ztri3or  9298  qtri3or  10245  trilpo  14830  trirec0  14831  reap0  14845
  Copyright terms: Public domain W3C validator