Theorem jaod 729

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 30	. . 3 |- ( ps -> ( ph -> ch ) )
3		jaod.2	. . . 4 |- ( ph -> ( th -> ch ) )
4	3	com12 30	. . 3 |- ( th -> ( ph -> ch ) )
5	2, 4	jaoi 728	. 2 |- ( ( ps \/ th ) -> ( ph -> ch ) )
6	5	com12 30	1 |- ( ph -> ( ( ps \/ th ) -> ch ) )

Syntax hints:   -> wi 4   \/ wo 720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  730  jaao  731  orel2  738  pm2.621  759  mtord  795  jaodan  809  pm2.63  812  pm2.74  819  dedlema  982  dedlemb  983  oplem1  988  ifnebibdc  3683  opthpr  3892  exmid1stab  4340  trsucss  4563  ordsucim  4642  onsucelsucr  4650  0elnn  4761  xpsspw  4882  relop  4925  fununi  5444  poxp  6458  nntri1  6759  nnsseleq  6764  nnmordi  6779  nnaordex  6791  nnm00  6793  swoord2  6827  nneneq  7148  exmidonfinlem  7535  elni2  7671  prubl  7843  distrlem4prl  7941  distrlem4pru  7942  ltxrlt  8381  recexre  8896  remulext1  8917  mulext1  8930  un0addcl  9575  un0mulcl  9576  elnnz  9633  zleloe  9670  zindd  9743  uzsplit  10477  fzm1  10485  expcl2lemap  10966  expnegzap  10988  expaddzap  10998  expmulzap  11000  qsqeqor  11065  nn0opthd  11138  facdiv  11154  facwordi  11156  bcpasc  11182  recvguniq  11739  absexpzap  11824  maxabslemval  11952  xrmaxiflemval  11994  sumrbdclem  12122  summodc  12128  zsumdc  12129  prodrbdclem  12316  zproddc  12324  prodssdc  12334  fprodcl2lem  12350  fprodsplitsn  12378  ordvdsmul  12579  gcdaddm  12739  nninfctlemfo  12795  lcmdvds  12835  dvdsprime  12878  prmdvdsexpr  12906  prmfac1  12908  pythagtriplem2  13023  4sqlem11  13158  unct  13311  domneq0  14554  gsumfsum  14895  baspartn  15074  reopnap  15570  coseq0q4123  15858  lgsdir2lem2  16062  upgrpredgv  16301  wlk1walkdom  16514  decidin  16739  bj-charfun  16747  bj-nntrans  16891  bj-nnelirr  16893  bj-findis  16919  triap  16983