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  4347  trsucss  4570  ordsucim  4649  onsucelsucr  4657  0elnn  4768  xpsspw  4889  relop  4932  fununi  5452  poxp  6472  nntri1  6774  nnsseleq  6779  nnmordi  6794  nnaordex  6806  nnm00  6808  swoord2  6842  nneneq  7164  exmidonfinlem  7551  elni2  7687  prubl  7859  distrlem4prl  7957  distrlem4pru  7958  ltxrlt  8397  recexre  8914  remulext1  8935  mulext1  8948  un0addcl  9607  un0mulcl  9608  elnnz  9663  zleloe  9700  zindd  9774  uzsplit  10515  fzm1  10523  expcl2lemap  11008  expnegzap  11030  expaddzap  11040  expmulzap  11042  qsqeqor  11107  nn0opthd  11181  facdiv  11197  facwordi  11199  bcpasc  11225  recvguniq  11782  absexpzap  11868  maxabslemval  11996  xrmaxiflemval  12040  sumrbdclem  12168  summodc  12174  zsumdc  12175  prodrbdclem  12362  zproddc  12370  prodssdc  12380  fprodcl2lem  12396  fprodsplitsn  12424  ordvdsmul  12625  gcdaddm  12785  nninfctlemfo  12841  lcmdvds  12881  dvdsprime  12924  prmdvdsexpr  12953  prmfac1  12955  pythagtriplem2  13073  4sqlem11  13208  prmlem0  13248  unct  13390  gsummptfidmsplit  14253  domneq0  14689  gsumfsum  15031  baspartn  15293  reopnap  15789  coseq0q4123  16078  rpcxpmul2z  16165  ppiublem1  16308  lgsdir2lem2  16370  upgrpredgv  16609  wlk1walkdom  16822  decidin  17047  bj-charfun  17055  bj-nntrans  17199  bj-nnelirr  17201  bj-findis  17227  triap  17301