Theorem jaod 722

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

Syntax hints:   -> wi 4   \/ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  723  jaao  724  orel2  731  pm2.621  752  mtord  788  jaodan  802  pm2.63  805  pm2.74  812  dedlema  975  dedlemb  976  oplem1  981  ifnebibdc  3648  opthpr  3850  exmid1stab  4292  trsucss  4514  ordsucim  4592  onsucelsucr  4600  0elnn  4711  xpsspw  4831  relop  4872  fununi  5389  poxp  6378  nntri1  6642  nnsseleq  6647  nnmordi  6662  nnaordex  6674  nnm00  6676  swoord2  6710  nneneq  7018  exmidonfinlem  7371  elni2  7501  prubl  7673  distrlem4prl  7771  distrlem4pru  7772  ltxrlt  8212  recexre  8725  remulext1  8746  mulext1  8759  un0addcl  9402  un0mulcl  9403  elnnz  9456  zleloe  9493  zindd  9565  uzsplit  10288  fzm1  10296  expcl2lemap  10773  expnegzap  10795  expaddzap  10805  expmulzap  10807  qsqeqor  10872  nn0opthd  10944  facdiv  10960  facwordi  10962  bcpasc  10988  recvguniq  11506  absexpzap  11591  maxabslemval  11719  xrmaxiflemval  11761  sumrbdclem  11888  summodc  11894  zsumdc  11895  prodrbdclem  12082  zproddc  12090  prodssdc  12100  fprodcl2lem  12116  fprodsplitsn  12144  ordvdsmul  12345  gcdaddm  12505  nninfctlemfo  12561  lcmdvds  12601  dvdsprime  12644  prmdvdsexpr  12672  prmfac1  12674  pythagtriplem2  12789  4sqlem11  12924  unct  13013  domneq0  14236  baspartn  14724  reopnap  15220  coseq0q4123  15508  lgsdir2lem2  15708  upgrpredgv  15944  wlk1walkdom  16070  decidin  16161  bj-charfun  16170  bj-nntrans  16314  bj-nnelirr  16316  bj-findis  16342  triap  16397