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  3601  opthpr  3799  exmid1stab  4238  trsucss  4455  ordsucim  4533  onsucelsucr  4541  0elnn  4652  xpsspw  4772  relop  4813  fununi  5323  poxp  6287  nntri1  6551  nnsseleq  6556  nnmordi  6571  nnaordex  6583  nnm00  6585  swoord2  6619  nneneq  6915  exmidonfinlem  7255  elni2  7376  prubl  7548  distrlem4prl  7646  distrlem4pru  7647  ltxrlt  8087  recexre  8599  remulext1  8620  mulext1  8633  un0addcl  9276  un0mulcl  9277  elnnz  9330  zleloe  9367  zindd  9438  uzsplit  10161  fzm1  10169  expcl2lemap  10625  expnegzap  10647  expaddzap  10657  expmulzap  10659  qsqeqor  10724  nn0opthd  10796  facdiv  10812  facwordi  10814  bcpasc  10840  recvguniq  11142  absexpzap  11227  maxabslemval  11355  xrmaxiflemval  11396  sumrbdclem  11523  summodc  11529  zsumdc  11530  prodrbdclem  11717  zproddc  11725  prodssdc  11735  fprodcl2lem  11751  fprodsplitsn  11779  ordvdsmul  11980  gcdaddm  12124  nninfctlemfo  12180  lcmdvds  12220  dvdsprime  12263  prmdvdsexpr  12291  prmfac1  12293  pythagtriplem2  12407  4sqlem11  12542  unct  12602  domneq0  13771  baspartn  14229  reopnap  14725  coseq0q4123  15010  lgsdir2lem2  15186  decidin  15359  bj-charfun  15369  bj-nntrans  15513  bj-nnelirr  15515  bj-findis  15541  triap  15589