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

Theorem mpjaodan 722
 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 721 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 406 1 (𝜑𝜒)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ∨ wo 639 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  mpjao3dan  1213  ifcldcd  3386  ordtri2or2exmidlem  4279  reg2exmidlema  4287  nndifsnid  6111  phpm  6358  fidifsnen  6362  fidifsnid  6363  fin0  6373  fientri3  6384  mullocprlem  6726  recexprlemloc  6787  z2ge  8840  fztri3or  9005  fzm1  9064  fzneuz  9065  qbtwnzlemstep  9205  rebtwn2zlemstep  9209  modifeq2int  9336  modsumfzodifsn  9346  expaddzaplem  9463  expnbnd  9540  bcval  9617  bccmpl  9622  ibcval5  9631  bcpasc  9634  bccl  9635  resqrexlemnm  9845  resqrexlemcvg  9846  resqrexlemoverl  9848  resqrexlemglsq  9849  leabs  9901  nn0abscl  9912  ltabs  9914  abslt  9915  fzomaxdif  9940  dvdsle  10156  mod2eq1n2dvds  10191  pw2dvdslemn  10253  nn0seqcvgd  10263
 Copyright terms: Public domain W3C validator