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	|- (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 635	. 2 |- ((ps \/ th) -> (ph -> ch))
6	5	com12 27	1 |- (ph -> ((ps \/ th) -> ch))

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