Theorem jaod 729

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

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjaod  730  jaao  731  orel2  738  pm2.621  759  mtord  795  jaodan  809  pm2.63  812  pm2.74  819  dedlema  982  dedlemb  983  oplem1  988  ifnebibdc  3686  opthpr  3897  exmid1stab  4345  trsucss  4568  ordsucim  4647  onsucelsucr  4655  0elnn  4766  xpsspw  4887  relop  4930  fununi  5449  poxp  6468  nntri1  6769  nnsseleq  6774  nnmordi  6789  nnaordex  6801  nnm00  6803  swoord2  6837  nneneq  7158  exmidonfinlem  7545  elni2  7681  prubl  7853  distrlem4prl  7951  distrlem4pru  7952  ltxrlt  8391  recexre  8908  remulext1  8929  mulext1  8942  un0addcl  9600  un0mulcl  9601  elnnz  9658  zleloe  9695  zindd  9768  uzsplit  10509  fzm1  10517  expcl2lemap  11001  expnegzap  11023  expaddzap  11033  expmulzap  11035  qsqeqor  11100  nn0opthd  11174  facdiv  11190  facwordi  11192  bcpasc  11218  recvguniq  11775  absexpzap  11861  maxabslemval  11989  xrmaxiflemval  12032  sumrbdclem  12160  summodc  12166  zsumdc  12167  prodrbdclem  12354  zproddc  12362  prodssdc  12372  fprodcl2lem  12388  fprodsplitsn  12416  ordvdsmul  12617  gcdaddm  12777  nninfctlemfo  12833  lcmdvds  12873  dvdsprime  12916  prmdvdsexpr  12945  prmfac1  12947  pythagtriplem2  13065  4sqlem11  13200  prmlem0  13240  unct  13382  domneq0  14630  gsumfsum  14972  baspartn  15200  reopnap  15696  coseq0q4123  15985  ppiublem1  16192  lgsdir2lem2  16246  upgrpredgv  16485  wlk1walkdom  16698  decidin  16923  bj-charfun  16931  bj-nntrans  17075  bj-nnelirr  17077  bj-findis  17103  triap  17176