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  6559  distrlem4pru  6560  ltxrlt  6862  recexre  7342  remulext1  7363  mulext1  7376  un0addcl  7971  un0mulcl  7972  elnnz  8011  zleloe  8048  zindd  8112  uzsplit  8704  fzm1  8712  expcl2lemap  8901  expnegzap  8923  expaddzap  8933  expmulzap  8935  bj-nntrans  9385  bj-nnelirr  9387  bj-findis  9409
  Copyright terms: Public domain W3C validator