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  3615  opthpr  3813  exmid1stab  4252  trsucss  4470  ordsucim  4548  onsucelsucr  4556  0elnn  4667  xpsspw  4787  relop  4828  fununi  5342  poxp  6318  nntri1  6582  nnsseleq  6587  nnmordi  6602  nnaordex  6614  nnm00  6616  swoord2  6650  nneneq  6954  exmidonfinlem  7301  elni2  7427  prubl  7599  distrlem4prl  7697  distrlem4pru  7698  ltxrlt  8138  recexre  8651  remulext1  8672  mulext1  8685  un0addcl  9328  un0mulcl  9329  elnnz  9382  zleloe  9419  zindd  9491  uzsplit  10214  fzm1  10222  expcl2lemap  10696  expnegzap  10718  expaddzap  10728  expmulzap  10730  qsqeqor  10795  nn0opthd  10867  facdiv  10883  facwordi  10885  bcpasc  10911  recvguniq  11306  absexpzap  11391  maxabslemval  11519  xrmaxiflemval  11561  sumrbdclem  11688  summodc  11694  zsumdc  11695  prodrbdclem  11882  zproddc  11890  prodssdc  11900  fprodcl2lem  11916  fprodsplitsn  11944  ordvdsmul  12145  gcdaddm  12305  nninfctlemfo  12361  lcmdvds  12401  dvdsprime  12444  prmdvdsexpr  12472  prmfac1  12474  pythagtriplem2  12589  4sqlem11  12724  unct  12813  domneq0  14034  baspartn  14522  reopnap  15018  coseq0q4123  15306  lgsdir2lem2  15506  decidin  15733  bj-charfun  15743  bj-nntrans  15887  bj-nnelirr  15889  bj-findis  15915  triap  15968