Theorem jaod 725

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

Syntax hints:   -> wi 4   \/ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  726  jaao  727  orel2  734  pm2.621  755  mtord  791  jaodan  805  pm2.63  808  pm2.74  815  dedlema  978  dedlemb  979  oplem1  984  ifnebibdc  3672  opthpr  3881  exmid1stab  4326  trsucss  4549  ordsucim  4627  onsucelsucr  4635  0elnn  4746  xpsspw  4867  relop  4910  fununi  5429  poxp  6441  nntri1  6742  nnsseleq  6747  nnmordi  6762  nnaordex  6774  nnm00  6776  swoord2  6810  nneneq  7124  exmidonfinlem  7509  elni2  7645  prubl  7817  distrlem4prl  7915  distrlem4pru  7916  ltxrlt  8355  recexre  8869  remulext1  8890  mulext1  8903  un0addcl  9546  un0mulcl  9547  elnnz  9604  zleloe  9641  zindd  9714  uzsplit  10448  fzm1  10456  expcl2lemap  10937  expnegzap  10959  expaddzap  10969  expmulzap  10971  qsqeqor  11036  nn0opthd  11109  facdiv  11125  facwordi  11127  bcpasc  11153  recvguniq  11705  absexpzap  11790  maxabslemval  11918  xrmaxiflemval  11960  sumrbdclem  12088  summodc  12094  zsumdc  12095  prodrbdclem  12282  zproddc  12290  prodssdc  12300  fprodcl2lem  12316  fprodsplitsn  12344  ordvdsmul  12545  gcdaddm  12705  nninfctlemfo  12761  lcmdvds  12801  dvdsprime  12844  prmdvdsexpr  12872  prmfac1  12874  pythagtriplem2  12989  4sqlem11  13124  unct  13277  domneq0  14519  baspartn  15041  reopnap  15537  coseq0q4123  15825  lgsdir2lem2  16028  upgrpredgv  16267  wlk1walkdom  16480  decidin  16695  bj-charfun  16703  bj-nntrans  16847  bj-nnelirr  16849  bj-findis  16875  triap  16939