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  3655  opthpr  3860  exmid1stab  4304  trsucss  4526  ordsucim  4604  onsucelsucr  4612  0elnn  4723  xpsspw  4844  relop  4886  fununi  5405  poxp  6406  nntri1  6707  nnsseleq  6712  nnmordi  6727  nnaordex  6739  nnm00  6741  swoord2  6775  nneneq  7086  exmidonfinlem  7464  elni2  7594  prubl  7766  distrlem4prl  7864  distrlem4pru  7865  ltxrlt  8304  recexre  8817  remulext1  8838  mulext1  8851  un0addcl  9494  un0mulcl  9495  elnnz  9550  zleloe  9587  zindd  9659  uzsplit  10389  fzm1  10397  expcl2lemap  10876  expnegzap  10898  expaddzap  10908  expmulzap  10910  qsqeqor  10975  nn0opthd  11047  facdiv  11063  facwordi  11065  bcpasc  11091  recvguniq  11635  absexpzap  11720  maxabslemval  11848  xrmaxiflemval  11890  sumrbdclem  12018  summodc  12024  zsumdc  12025  prodrbdclem  12212  zproddc  12220  prodssdc  12230  fprodcl2lem  12246  fprodsplitsn  12274  ordvdsmul  12475  gcdaddm  12635  nninfctlemfo  12691  lcmdvds  12731  dvdsprime  12774  prmdvdsexpr  12802  prmfac1  12804  pythagtriplem2  12919  4sqlem11  13054  unct  13143  domneq0  14368  baspartn  14861  reopnap  15357  coseq0q4123  15645  lgsdir2lem2  15848  upgrpredgv  16087  wlk1walkdom  16300  decidin  16515  bj-charfun  16523  bj-nntrans  16667  bj-nnelirr  16669  bj-findis  16695  triap  16761