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

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 |- ( ph -> ( ps -> ch ) )
2	1	com12 27	. . 3 |- ( ps -> ( ph -> ch ) )
3		jaod.2	. . . 4 |- ( ph -> ( th -> ch ) )
4	3	com12 27	. . 3 |- ( th -> ( ph -> ch ) )
5	2, 4	jaoi 636	. 2 |- ( ( ps \/ th ) -> ( ph -> ch ) )
6	5	com12 27	1 |- ( ph -> ( ( ps \/ th ) -> ch ) )

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