ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jaod Unicode 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  6469  distrlem4prl  6560  distrlem4pru  6561  ltxrlt  6882  recexre  7362  remulext1  7383  mulext1  7396  un0addcl  7991  un0mulcl  7992  elnnz  8031  zleloe  8068  zindd  8132  uzsplit  8724  fzm1  8732  expcl2lemap  8921  expnegzap  8943  expaddzap  8953  expmulzap  8955  bj-nntrans  9411  bj-nnelirr  9413  bj-findis  9439
  Copyright terms: Public domain W3C validator