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

Theorem mpjaodan 711
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination). (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaodan.1 ((𝜑𝜓) → 𝜒)
jaodan.2 ((𝜑𝜃) → 𝜒)
jaodan.3 (𝜑 → (𝜓𝜃))
Assertion
Ref Expression
mpjaodan (𝜑𝜒)

Proof of Theorem mpjaodan
StepHypRef Expression
1 jaodan.3 . 2 (𝜑 → (𝜓𝜃))
2 jaodan.1 . . 3 ((𝜑𝜓) → 𝜒)
3 jaodan.2 . . 3 ((𝜑𝜃) → 𝜒)
42, 3jaodan 710 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 398 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wo 629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpjao3dan  1202  ifcldcd  3355  ordtri2or2exmidlem  4223  nndifsnid  6043  phpm  6290  fidifsnen  6294  fidifsnid  6295  fin0  6305  fientri3  6315  mullocprlem  6625  recexprlemloc  6686  z2ge  8682  fztri3or  8846  fzm1  8905  fzneuz  8906  expaddzaplem  9152  expnbnd  9226  resqrexlemnm  9470  resqrexlemcvg  9471  resqrexlemoverl  9473  resqrexlemglsq  9474  leabs  9526  nn0abscl  9535  ltabs  9537  abslt  9538  fzomaxdif  9563  nn0seqcvgd  9733
  Copyright terms: Public domain W3C validator