Theorem jaod 707

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

Syntax hints:   -> wi 4   \/ wo 698

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaod  708  jaao  709  orel2  716  pm2.621  737  mtord  773  jaodan  787  pm2.63  790  pm2.74  797  dedlema  954  dedlemb  955  oplem1  960  opthpr  3707  trsucss  4353  ordsucim  4424  onsucelsucr  4432  0elnn  4540  xpsspw  4659  relop  4697  fununi  5199  poxp  6137  nntri1  6400  nnsseleq  6405  nnmordi  6420  nnaordex  6431  nnm00  6433  swoord2  6467  nneneq  6759  exmidonfinlem  7066  elni2  7146  prubl  7318  distrlem4prl  7416  distrlem4pru  7417  ltxrlt  7854  recexre  8364  remulext1  8385  mulext1  8398  un0addcl  9034  un0mulcl  9035  elnnz  9088  zleloe  9125  zindd  9193  uzsplit  9903  fzm1  9911  expcl2lemap  10336  expnegzap  10358  expaddzap  10368  expmulzap  10370  nn0opthd  10500  facdiv  10516  facwordi  10518  bcpasc  10544  recvguniq  10799  absexpzap  10884  maxabslemval  11012  xrmaxiflemval  11051  sumrbdclem  11178  summodc  11184  zsumdc  11185  prodrbdclem  11372  zproddc  11380  ordvdsmul  11570  gcdaddm  11708  lcmdvds  11796  dvdsprime  11839  prmdvdsexpr  11864  prmfac1  11866  unct  11991  baspartn  12256  reopnap  12746  coseq0q4123  12963  decidin  13175  bj-nntrans  13320  bj-nnelirr  13322  bj-findis  13348  exmid1stab  13368  triap  13399