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  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