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

Theorem mpjao3dan 1243
Description: Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.)
Hypotheses
Ref Expression
mpjao3dan.1 ((𝜑𝜓) → 𝜒)
mpjao3dan.2 ((𝜑𝜃) → 𝜒)
mpjao3dan.3 ((𝜑𝜏) → 𝜒)
mpjao3dan.4 (𝜑 → (𝜓𝜃𝜏))
Assertion
Ref Expression
mpjao3dan (𝜑𝜒)

Proof of Theorem mpjao3dan
StepHypRef Expression
1 mpjao3dan.1 . . 3 ((𝜑𝜓) → 𝜒)
2 mpjao3dan.2 . . 3 ((𝜑𝜃) → 𝜒)
31, 2jaodan 746 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
4 mpjao3dan.3 . 2 ((𝜑𝜏) → 𝜒)
5 mpjao3dan.4 . . 3 (𝜑 → (𝜓𝜃𝜏))
6 df-3or 925 . . 3 ((𝜓𝜃𝜏) ↔ ((𝜓𝜃) ∨ 𝜏))
75, 6sylib 120 . 2 (𝜑 → ((𝜓𝜃) ∨ 𝜏))
83, 4, 7mpjaodan 747 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wo 664  w3o 923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665
This theorem depends on definitions:  df-bi 115  df-3or 925
This theorem is referenced by:  wetriext  4382  nntri3  6240  nntri2or2  6241  tridc  6595  caucvgprlemnkj  7204  caucvgprlemnbj  7205  caucvgprprlemnkj  7230  caucvgprprlemnbj  7231  caucvgsr  7326  addmodlteq  9770  iseqf1olemkle  9878  hashfiv01gt1  10155  zdvdsdc  10899  divalglemeunn  11003  divalglemex  11004  divalglemeuneg  11005  divalg  11006  znege1  11238  nninfalllemn  11544
  Copyright terms: Public domain W3C validator