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

Theorem mpjao3dan 1239
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 744 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
4 mpjao3dan.3 . 2 ((𝜑𝜏) → 𝜒)
5 mpjao3dan.4 . . 3 (𝜑 → (𝜓𝜃𝜏))
6 df-3or 921 . . 3 ((𝜓𝜃𝜏) ↔ ((𝜓𝜃) ∨ 𝜏))
75, 6sylib 120 . 2 (𝜑 → ((𝜓𝜃) ∨ 𝜏))
83, 4, 7mpjaodan 745 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wo 662  w3o 919
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 663
This theorem depends on definitions:  df-bi 115  df-3or 921
This theorem is referenced by:  wetriext  4327  nntri3  6141  nntri2or2  6142  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprprlemnkj  6944  caucvgprprlemnbj  6945  caucvgsr  7040  addmodlteq  9480  sizefiv01gt1  9806  zdvdsdc  10361  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467  divalg  10468  znege1  10700
  Copyright terms: Public domain W3C validator