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

Theorem mpjao3dan 1302
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 792 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
4 mpjao3dan.3 . 2 ((𝜑𝜏) → 𝜒)
5 mpjao3dan.4 . . 3 (𝜑 → (𝜓𝜃𝜏))
6 df-3or 974 . . 3 ((𝜓𝜃𝜏) ↔ ((𝜓𝜃) ∨ 𝜏))
75, 6sylib 121 . 2 (𝜑 → ((𝜓𝜃) ∨ 𝜏))
83, 4, 7mpjaodan 793 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wo 703  w3o 972
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 704
This theorem depends on definitions:  df-bi 116  df-3or 974
This theorem is referenced by:  wetriext  4561  nntri3  6476  nntri2or2  6477  nntr2  6482  tridc  6877  nnnninfeq  7104  exmidontriimlem2  7199  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprprlemnkj  7654  caucvgprprlemnbj  7655  caucvgsr  7764  npnflt  9772  nmnfgt  9775  xleadd1a  9830  xltadd1  9833  xlt2add  9837  xsubge0  9838  xleaddadd  9844  addmodlteq  10354  iseqf1olemkle  10440  hashfiv01gt1  10716  xrmaxltsup  11221  xrmaxadd  11224  xrbdtri  11239  cvgratz  11495  zdvdsdc  11774  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  divalg  11883  znege1  12132  ennnfonelemk  12355  isxmet2d  13142  trilpolemres  14074  trirec0  14076
  Copyright terms: Public domain W3C validator