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  3649  opthpr  3851  exmid1stab  4294  trsucss  4516  ordsucim  4594  onsucelsucr  4602  0elnn  4713  xpsspw  4834  relop  4876  fununi  5393  poxp  6390  nntri1  6657  nnsseleq  6662  nnmordi  6677  nnaordex  6689  nnm00  6691  swoord2  6725  nneneq  7036  exmidonfinlem  7392  elni2  7522  prubl  7694  distrlem4prl  7792  distrlem4pru  7793  ltxrlt  8233  recexre  8746  remulext1  8767  mulext1  8780  un0addcl  9423  un0mulcl  9424  elnnz  9477  zleloe  9514  zindd  9586  uzsplit  10315  fzm1  10323  expcl2lemap  10801  expnegzap  10823  expaddzap  10833  expmulzap  10835  qsqeqor  10900  nn0opthd  10972  facdiv  10988  facwordi  10990  bcpasc  11016  recvguniq  11543  absexpzap  11628  maxabslemval  11756  xrmaxiflemval  11798  sumrbdclem  11925  summodc  11931  zsumdc  11932  prodrbdclem  12119  zproddc  12127  prodssdc  12137  fprodcl2lem  12153  fprodsplitsn  12181  ordvdsmul  12382  gcdaddm  12542  nninfctlemfo  12598  lcmdvds  12638  dvdsprime  12681  prmdvdsexpr  12709  prmfac1  12711  pythagtriplem2  12826  4sqlem11  12961  unct  13050  domneq0  14273  baspartn  14761  reopnap  15257  coseq0q4123  15545  lgsdir2lem2  15745  upgrpredgv  15981  wlk1walkdom  16147  decidin  16303  bj-charfun  16312  bj-nntrans  16456  bj-nnelirr  16458  bj-findis  16484  triap  16543