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  6384  nntri1  6650  nnsseleq  6655  nnmordi  6670  nnaordex  6682  nnm00  6684  swoord2  6718  nneneq  7026  exmidonfinlem  7382  elni2  7512  prubl  7684  distrlem4prl  7782  distrlem4pru  7783  ltxrlt  8223  recexre  8736  remulext1  8757  mulext1  8770  un0addcl  9413  un0mulcl  9414  elnnz  9467  zleloe  9504  zindd  9576  uzsplit  10300  fzm1  10308  expcl2lemap  10785  expnegzap  10807  expaddzap  10817  expmulzap  10819  qsqeqor  10884  nn0opthd  10956  facdiv  10972  facwordi  10974  bcpasc  11000  recvguniq  11522  absexpzap  11607  maxabslemval  11735  xrmaxiflemval  11777  sumrbdclem  11904  summodc  11910  zsumdc  11911  prodrbdclem  12098  zproddc  12106  prodssdc  12116  fprodcl2lem  12132  fprodsplitsn  12160  ordvdsmul  12361  gcdaddm  12521  nninfctlemfo  12577  lcmdvds  12617  dvdsprime  12660  prmdvdsexpr  12688  prmfac1  12690  pythagtriplem2  12805  4sqlem11  12940  unct  13029  domneq0  14252  baspartn  14740  reopnap  15236  coseq0q4123  15524  lgsdir2lem2  15724  upgrpredgv  15960  wlk1walkdom  16105  decidin  16244  bj-charfun  16253  bj-nntrans  16397  bj-nnelirr  16399  bj-findis  16425  triap  16485