Theorem jaod 719

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

Syntax hints:   -> wi 4   \/ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  720  jaao  721  orel2  728  pm2.621  749  mtord  785  jaodan  799  pm2.63  802  pm2.74  809  dedlema  972  dedlemb  973  oplem1  978  ifnebibdc  3625  opthpr  3826  exmid1stab  4268  trsucss  4488  ordsucim  4566  onsucelsucr  4574  0elnn  4685  xpsspw  4805  relop  4846  fununi  5361  poxp  6341  nntri1  6605  nnsseleq  6610  nnmordi  6625  nnaordex  6637  nnm00  6639  swoord2  6673  nneneq  6979  exmidonfinlem  7332  elni2  7462  prubl  7634  distrlem4prl  7732  distrlem4pru  7733  ltxrlt  8173  recexre  8686  remulext1  8707  mulext1  8720  un0addcl  9363  un0mulcl  9364  elnnz  9417  zleloe  9454  zindd  9526  uzsplit  10249  fzm1  10257  expcl2lemap  10733  expnegzap  10755  expaddzap  10765  expmulzap  10767  qsqeqor  10832  nn0opthd  10904  facdiv  10920  facwordi  10922  bcpasc  10948  recvguniq  11421  absexpzap  11506  maxabslemval  11634  xrmaxiflemval  11676  sumrbdclem  11803  summodc  11809  zsumdc  11810  prodrbdclem  11997  zproddc  12005  prodssdc  12015  fprodcl2lem  12031  fprodsplitsn  12059  ordvdsmul  12260  gcdaddm  12420  nninfctlemfo  12476  lcmdvds  12516  dvdsprime  12559  prmdvdsexpr  12587  prmfac1  12589  pythagtriplem2  12704  4sqlem11  12839  unct  12928  domneq0  14149  baspartn  14637  reopnap  15133  coseq0q4123  15421  lgsdir2lem2  15621  upgrpredgv  15850  decidin  15933  bj-charfun  15942  bj-nntrans  16086  bj-nnelirr  16088  bj-findis  16114  triap  16170