Theorem jaod 670

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

Syntax hints:   -> wi 4   \/ wo 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpjaod  671  jaao  672  orel2  678  pm2.621  699  mtord  730  jaodan  744  pm2.63  747  pm2.74  754  dedlema  911  dedlemb  912  oplem1  917  opthpr  3572  trsucss  4186  ordsucim  4252  onsucelsucr  4260  0elnn  4366  xpsspw  4478  relop  4514  fununi  4998  poxp  5884  nntri1  6140  nnsseleq  6145  nnmordi  6155  nnaordex  6166  nnm00  6168  swoord2  6202  nneneq  6392  elni2  6566  prubl  6738  distrlem4prl  6836  distrlem4pru  6837  ltxrlt  7245  recexre  7745  remulext1  7766  mulext1  7779  un0addcl  8388  un0mulcl  8389  elnnz  8442  zleloe  8479  zindd  8546  uzsplit  9185  fzm1  9193  expcl2lemap  9585  expnegzap  9607  expaddzap  9617  expmulzap  9619  nn0opthd  9746  facdiv  9762  facwordi  9764  bcpasc  9790  recvguniq  10019  absexpzap  10104  maxabslemval  10232  isumrblem  10337  ordvdsmul  10381  gcdaddm  10519  lcmdvds  10605  dvdsprime  10648  prmdvdsexpr  10673  prmfac1  10675  decidin  10758  bj-nntrans  10904  bj-nnelirr  10906  bj-findis  10932