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  4253  trsucss  4471  ordsucim  4549  onsucelsucr  4557  0elnn  4668  xpsspw  4788  relop  4829  fununi  5343  poxp  6320  nntri1  6584  nnsseleq  6589  nnmordi  6604  nnaordex  6616  nnm00  6618  swoord2  6652  nneneq  6956  exmidonfinlem  7303  elni2  7429  prubl  7601  distrlem4prl  7699  distrlem4pru  7700  ltxrlt  8140  recexre  8653  remulext1  8674  mulext1  8687  un0addcl  9330  un0mulcl  9331  elnnz  9384  zleloe  9421  zindd  9493  uzsplit  10216  fzm1  10224  expcl2lemap  10698  expnegzap  10720  expaddzap  10730  expmulzap  10732  qsqeqor  10797  nn0opthd  10869  facdiv  10885  facwordi  10887  bcpasc  10913  recvguniq  11339  absexpzap  11424  maxabslemval  11552  xrmaxiflemval  11594  sumrbdclem  11721  summodc  11727  zsumdc  11728  prodrbdclem  11915  zproddc  11923  prodssdc  11933  fprodcl2lem  11949  fprodsplitsn  11977  ordvdsmul  12178  gcdaddm  12338  nninfctlemfo  12394  lcmdvds  12434  dvdsprime  12477  prmdvdsexpr  12505  prmfac1  12507  pythagtriplem2  12622  4sqlem11  12757  unct  12846  domneq0  14067  baspartn  14555  reopnap  15051  coseq0q4123  15339  lgsdir2lem2  15539  decidin  15770  bj-charfun  15780  bj-nntrans  15924  bj-nnelirr  15926  bj-findis  15952  triap  16005