Theorem jaod 712

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

Syntax hints:   -> wi 4   \/ wo 703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaod  713  jaao  714  orel2  721  pm2.621  742  mtord  778  jaodan  792  pm2.63  795  pm2.74  802  dedlema  964  dedlemb  965  oplem1  970  opthpr  3759  trsucss  4408  ordsucim  4484  onsucelsucr  4492  0elnn  4603  xpsspw  4723  relop  4761  fununi  5266  poxp  6211  nntri1  6475  nnsseleq  6480  nnmordi  6495  nnaordex  6507  nnm00  6509  swoord2  6543  nneneq  6835  exmidonfinlem  7170  elni2  7276  prubl  7448  distrlem4prl  7546  distrlem4pru  7547  ltxrlt  7985  recexre  8497  remulext1  8518  mulext1  8531  un0addcl  9168  un0mulcl  9169  elnnz  9222  zleloe  9259  zindd  9330  uzsplit  10048  fzm1  10056  expcl2lemap  10488  expnegzap  10510  expaddzap  10520  expmulzap  10522  qsqeqor  10586  nn0opthd  10656  facdiv  10672  facwordi  10674  bcpasc  10700  recvguniq  10959  absexpzap  11044  maxabslemval  11172  xrmaxiflemval  11213  sumrbdclem  11340  summodc  11346  zsumdc  11347  prodrbdclem  11534  zproddc  11542  prodssdc  11552  fprodcl2lem  11568  fprodsplitsn  11596  ordvdsmul  11796  gcdaddm  11939  lcmdvds  12033  dvdsprime  12076  prmdvdsexpr  12104  prmfac1  12106  pythagtriplem2  12220  unct  12397  baspartn  12842  reopnap  13332  coseq0q4123  13549  lgsdir2lem2  13724  decidin  13832  bj-charfun  13842  bj-nntrans  13986  bj-nnelirr  13988  bj-findis  14014  exmid1stab  14033  triap  14061