Theorem jaod 717

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

Syntax hints:   -> wi 4   \/ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  718  jaao  719  orel2  726  pm2.621  747  mtord  783  jaodan  797  pm2.63  800  pm2.74  807  dedlema  969  dedlemb  970  oplem1  975  opthpr  3774  exmid1stab  4210  trsucss  4425  ordsucim  4501  onsucelsucr  4509  0elnn  4620  xpsspw  4740  relop  4779  fununi  5286  poxp  6235  nntri1  6499  nnsseleq  6504  nnmordi  6519  nnaordex  6531  nnm00  6533  swoord2  6567  nneneq  6859  exmidonfinlem  7194  elni2  7315  prubl  7487  distrlem4prl  7585  distrlem4pru  7586  ltxrlt  8025  recexre  8537  remulext1  8558  mulext1  8571  un0addcl  9211  un0mulcl  9212  elnnz  9265  zleloe  9302  zindd  9373  uzsplit  10094  fzm1  10102  expcl2lemap  10534  expnegzap  10556  expaddzap  10566  expmulzap  10568  qsqeqor  10633  nn0opthd  10704  facdiv  10720  facwordi  10722  bcpasc  10748  recvguniq  11006  absexpzap  11091  maxabslemval  11219  xrmaxiflemval  11260  sumrbdclem  11387  summodc  11393  zsumdc  11394  prodrbdclem  11581  zproddc  11589  prodssdc  11599  fprodcl2lem  11615  fprodsplitsn  11643  ordvdsmul  11843  gcdaddm  11987  lcmdvds  12081  dvdsprime  12124  prmdvdsexpr  12152  prmfac1  12154  pythagtriplem2  12268  unct  12445  baspartn  13589  reopnap  14077  coseq0q4123  14294  lgsdir2lem2  14469  decidin  14588  bj-charfun  14598  bj-nntrans  14742  bj-nnelirr  14744  bj-findis  14770  triap  14816