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  954  dedlemb  955  oplem1  960  opthpr  3735  trsucss  4383  ordsucim  4459  onsucelsucr  4467  0elnn  4578  xpsspw  4698  relop  4736  fununi  5238  poxp  6179  nntri1  6443  nnsseleq  6448  nnmordi  6463  nnaordex  6474  nnm00  6476  swoord2  6510  nneneq  6802  exmidonfinlem  7128  elni2  7234  prubl  7406  distrlem4prl  7504  distrlem4pru  7505  ltxrlt  7943  recexre  8453  remulext1  8474  mulext1  8487  un0addcl  9123  un0mulcl  9124  elnnz  9177  zleloe  9214  zindd  9282  uzsplit  9994  fzm1  10002  expcl2lemap  10431  expnegzap  10453  expaddzap  10463  expmulzap  10465  nn0opthd  10596  facdiv  10612  facwordi  10614  bcpasc  10640  recvguniq  10895  absexpzap  10980  maxabslemval  11108  xrmaxiflemval  11147  sumrbdclem  11274  summodc  11280  zsumdc  11281  prodrbdclem  11468  zproddc  11476  prodssdc  11486  fprodcl2lem  11502  fprodsplitsn  11530  ordvdsmul  11727  gcdaddm  11867  lcmdvds  11955  dvdsprime  11998  prmdvdsexpr  12024  prmfac1  12026  unct  12171  baspartn  12448  reopnap  12938  coseq0q4123  13155  decidin  13371  bj-charfun  13382  bj-nntrans  13526  bj-nnelirr  13528  bj-findis  13554  exmid1stab  13572  triap  13600