Theorem jaod 724

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

Syntax hints:   -> wi 4   \/ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  725  jaao  726  orel2  733  pm2.621  754  mtord  790  jaodan  804  pm2.63  807  pm2.74  814  dedlema  977  dedlemb  978  oplem1  983  ifnebibdc  3651  opthpr  3855  exmid1stab  4298  trsucss  4520  ordsucim  4598  onsucelsucr  4606  0elnn  4717  xpsspw  4838  relop  4880  fununi  5398  poxp  6397  nntri1  6664  nnsseleq  6669  nnmordi  6684  nnaordex  6696  nnm00  6698  swoord2  6732  nneneq  7043  exmidonfinlem  7404  elni2  7534  prubl  7706  distrlem4prl  7804  distrlem4pru  7805  ltxrlt  8245  recexre  8758  remulext1  8779  mulext1  8792  un0addcl  9435  un0mulcl  9436  elnnz  9489  zleloe  9526  zindd  9598  uzsplit  10327  fzm1  10335  expcl2lemap  10814  expnegzap  10836  expaddzap  10846  expmulzap  10848  qsqeqor  10913  nn0opthd  10985  facdiv  11001  facwordi  11003  bcpasc  11029  recvguniq  11573  absexpzap  11658  maxabslemval  11786  xrmaxiflemval  11828  sumrbdclem  11956  summodc  11962  zsumdc  11963  prodrbdclem  12150  zproddc  12158  prodssdc  12168  fprodcl2lem  12184  fprodsplitsn  12212  ordvdsmul  12413  gcdaddm  12573  nninfctlemfo  12629  lcmdvds  12669  dvdsprime  12712  prmdvdsexpr  12740  prmfac1  12742  pythagtriplem2  12857  4sqlem11  12992  unct  13081  domneq0  14305  baspartn  14793  reopnap  15289  coseq0q4123  15577  lgsdir2lem2  15777  upgrpredgv  16016  wlk1walkdom  16229  decidin  16444  bj-charfun  16453  bj-nntrans  16597  bj-nnelirr  16599  bj-findis  16625  triap  16684