Theorem jaod 707

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

Syntax hints:   -> wi 4   \/ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaod  708  jaao  709  orel2  716  pm2.621  737  mtord  773  jaodan  787  pm2.63  790  pm2.74  797  dedlema  959  dedlemb  960  oplem1  965  opthpr  3751  trsucss  4400  ordsucim  4476  onsucelsucr  4484  0elnn  4595  xpsspw  4715  relop  4753  fununi  5255  poxp  6196  nntri1  6460  nnsseleq  6465  nnmordi  6480  nnaordex  6491  nnm00  6493  swoord2  6527  nneneq  6819  exmidonfinlem  7145  elni2  7251  prubl  7423  distrlem4prl  7521  distrlem4pru  7522  ltxrlt  7960  recexre  8472  remulext1  8493  mulext1  8506  un0addcl  9143  un0mulcl  9144  elnnz  9197  zleloe  9234  zindd  9305  uzsplit  10023  fzm1  10031  expcl2lemap  10463  expnegzap  10485  expaddzap  10495  expmulzap  10497  qsqeqor  10561  nn0opthd  10631  facdiv  10647  facwordi  10649  bcpasc  10675  recvguniq  10933  absexpzap  11018  maxabslemval  11146  xrmaxiflemval  11187  sumrbdclem  11314  summodc  11320  zsumdc  11321  prodrbdclem  11508  zproddc  11516  prodssdc  11526  fprodcl2lem  11542  fprodsplitsn  11570  ordvdsmul  11770  gcdaddm  11913  lcmdvds  12007  dvdsprime  12050  prmdvdsexpr  12078  prmfac1  12080  pythagtriplem2  12194  unct  12371  baspartn  12648  reopnap  13138  coseq0q4123  13355  lgsdir2lem2  13530  decidin  13638  bj-charfun  13649  bj-nntrans  13793  bj-nnelirr  13795  bj-findis  13821  exmid1stab  13840  triap  13868