Theorem jaod 718

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

Syntax hints:   -> wi 4   \/ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  719  jaao  720  orel2  727  pm2.621  748  mtord  784  jaodan  798  pm2.63  801  pm2.74  808  dedlema  971  dedlemb  972  oplem1  977  ifnebibdc  3604  opthpr  3802  exmid1stab  4241  trsucss  4458  ordsucim  4536  onsucelsucr  4544  0elnn  4655  xpsspw  4775  relop  4816  fununi  5326  poxp  6290  nntri1  6554  nnsseleq  6559  nnmordi  6574  nnaordex  6586  nnm00  6588  swoord2  6622  nneneq  6918  exmidonfinlem  7260  elni2  7381  prubl  7553  distrlem4prl  7651  distrlem4pru  7652  ltxrlt  8092  recexre  8605  remulext1  8626  mulext1  8639  un0addcl  9282  un0mulcl  9283  elnnz  9336  zleloe  9373  zindd  9444  uzsplit  10167  fzm1  10175  expcl2lemap  10643  expnegzap  10665  expaddzap  10675  expmulzap  10677  qsqeqor  10742  nn0opthd  10814  facdiv  10830  facwordi  10832  bcpasc  10858  recvguniq  11160  absexpzap  11245  maxabslemval  11373  xrmaxiflemval  11415  sumrbdclem  11542  summodc  11548  zsumdc  11549  prodrbdclem  11736  zproddc  11744  prodssdc  11754  fprodcl2lem  11770  fprodsplitsn  11798  ordvdsmul  11999  gcdaddm  12151  nninfctlemfo  12207  lcmdvds  12247  dvdsprime  12290  prmdvdsexpr  12318  prmfac1  12320  pythagtriplem2  12435  4sqlem11  12570  unct  12659  domneq0  13828  baspartn  14286  reopnap  14782  coseq0q4123  15070  lgsdir2lem2  15270  decidin  15443  bj-charfun  15453  bj-nntrans  15597  bj-nnelirr  15599  bj-findis  15625  triap  15673