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

Theorem jaod 636
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)
Hypotheses
Ref Expression
jaod.1 (φ → (ψχ))
jaod.2 (φ → (θχ))
Assertion
Ref Expression
jaod (φ → ((ψ θ) → χ))

Proof of Theorem jaod
StepHypRef Expression
1 jaod.1 . . . 4 (φ → (ψχ))
21com12 27 . . 3 (ψ → (φχ))
3 jaod.2 . . . 4 (φ → (θχ))
43com12 27 . . 3 (θ → (φχ))
52, 4jaoi 635 . 2 ((ψ θ) → (φχ))
65com12 27 1 (φ → ((ψ θ) → χ))
Colors of variables: wff set class
Syntax hints:  wi 4   wo 628
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 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpjaod  637  jaao  638  orel2  644  pm2.621  665  mtord  696  jaodan  709  pm2.63  712  pm2.74  719  dedlema  875  dedlemb  876  oplem1  881  opthpr  3534  trsucss  4126  ordsucim  4192  onsucelsucr  4199  0elnn  4283  xpsspw  4393  relop  4429  fununi  4910  poxp  5794  nntri1  6013  nnmordi  6025  nnaordex  6036  nnm00  6038  swoord2  6072  elni2  6298  prubl  6468  distrlem4prl  6558  distrlem4pru  6559  ltxrlt  6842  recexre  7322  remulext1  7343  mulext1  7356  un0addcl  7951  un0mulcl  7952  elnnz  7991  zleloe  8028  zindd  8092  uzsplit  8684  fzm1  8692  expcl2lemap  8881  expnegzap  8903  expaddzap  8913  expmulzap  8915  bj-nntrans  9339  bj-nnelirr  9341  bj-findis  9363
  Copyright terms: Public domain W3C validator