ILE Home 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  |-  ( ph  ->  ( ps  ->  ch ) )
jaod.2  |-  ( ph  ->  ( th  ->  ch ) )
Assertion
Ref Expression
jaod  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)

Proof of Theorem jaod
StepHypRef Expression
1 jaod.1 . . . 4  |-  ( ph  ->  ( ps  ->  ch ) )
21com12 27 . . 3  |-  ( ps 
->  ( ph  ->  ch ) )
3 jaod.2 . . . 4  |-  ( ph  ->  ( th  ->  ch ) )
43com12 27 . . 3  |-  ( th 
->  ( ph  ->  ch ) )
52, 4jaoi 636 . 2  |-  ( ( ps  \/  th )  ->  ( ph  ->  ch ) )
65com12 27 1  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
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  3540  trsucss  4156  ordsucim  4222  onsucelsucr  4230  0elnn  4327  xpsspw  4437  relop  4473  fununi  4954  poxp  5840  nntri1  6061  nnsseleq  6066  nnmordi  6076  nnaordex  6087  nnm00  6089  swoord2  6123  nneneq  6307  elni2  6393  prubl  6565  distrlem4prl  6663  distrlem4pru  6664  ltxrlt  7065  recexre  7545  remulext1  7566  mulext1  7579  un0addcl  8187  un0mulcl  8188  elnnz  8227  zleloe  8264  zindd  8328  uzsplit  8921  fzm1  8929  expcl2lemap  9145  expnegzap  9167  expaddzap  9177  expmulzap  9179  recvguniq  9471  absexpzap  9554  bj-nntrans  9949  bj-nnelirr  9951  bj-findis  9977
  Copyright terms: Public domain W3C validator