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

Theorem jaod 637
 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 636 . 2
65com12 27 1
 Colors of variables: wff set class Syntax hints:   wi 4   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:  mpjaod  638  jaao  639  orel2  645  pm2.621  666  mtord  697  jaodan  710  pm2.63  713  pm2.74  720  dedlema  876  dedlemb  877  oplem1  882  opthpr  3543  trsucss  4160  ordsucim  4226  onsucelsucr  4234  0elnn  4340  xpsspw  4450  relop  4486  fununi  4967  poxp  5853  nntri1  6074  nnsseleq  6079  nnmordi  6089  nnaordex  6100  nnm00  6102  swoord2  6136  nneneq  6320  elni2  6412  prubl  6584  distrlem4prl  6682  distrlem4pru  6683  ltxrlt  7085  recexre  7569  remulext1  7590  mulext1  7603  un0addcl  8215  un0mulcl  8216  elnnz  8255  zleloe  8292  zindd  8356  uzsplit  8954  fzm1  8962  expcl2lemap  9267  expnegzap  9289  expaddzap  9299  expmulzap  9301  recvguniq  9593  absexpzap  9676  bj-nntrans  10076  bj-nnelirr  10078  bj-findis  10104
 Copyright terms: Public domain W3C validator