Theorem jaoi 635

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)

Hypotheses

Ref	Expression
jaoi.1	|- (ph -> ps)
jaoi.2	|- (ch -> ps)

Assertion

Ref	Expression
jaoi	|- ((ph \/ ch) -> ps)

Proof of Theorem jaoi

Step	Hyp	Ref	Expression
1		jaoi.1	. 2 |- (ph -> ps)
2		jaoi.2	. 2 |- (ch -> ps)
3		pm3.44 634	. 2 |- (((ph -> ps) /\ (ch -> ps)) -> ((ph \/ ch) -> ps))
4	1, 2, 3	mp2an 402	1 |- ((ph \/ ch) -> ps)

Syntax hints:   -> wi 4   \/ wo 628

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  jaod  636  jaoa  639  pm2.53  640  pm1.4  645  imorri  667  ioran  668  pm3.14  669  pm1.2  672  orim12i  675  pm1.5  681  pm2.41  692  pm2.42  693  pm2.4  694  pm4.44  695  jaoian  708  pm2.64  713  pm2.76  720  pm2.82  724  pm3.2ni  725  andi  730  condc  748  pm2.61ddc  757  pm5.18dc  776  dcim  783  imorr  796  pm4.78i  807  pm2.85dc  810  peircedc  819  dcan  841  dcor  842  pm4.42r  877  oplem1  881  xoranor  1267  biassdc  1283  anxordi  1288  19.33  1370  hbequid  1403  hbor  1435  19.30dc  1515  19.43  1516  19.32r  1567  hbae  1603  equvini  1638  equveli  1639  exdistrfor  1678  dveeq2  1693  dveeq2or  1694  sbequi  1717  nfsbxy  1815  nfsbxyt  1816  sbcomxyyz  1843  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  modc  1940  mooran1  1969  moexexdc  1981  rgen2a  2369  r19.32r  2451  eueq2dc  2708  eueq3dc  2709  sbcor  2801  sspssr  3037  elun  3078  ssun  3116  inss  3160  undif3ss  3192  elpr2  3386  sssnr  3515  ssprr  3518  sstpr  3519  preq12b  3532  copsexg  3972  sotritric  4052  regexmidlem1  4218  nn0eln0  4284  xpeq0r  4689  funtpg  4893  acexmidlemcase  5450  acexmidlem2  5452  nnm00  6038  renfdisj  6856  nn0ge0  7963  elnnnn0b  7982  elnn0z  8014  nn0n0n1ge2b  8076  nn0ind-raph  8111  uzin  8261  elnn1uz2  8300  indstr2  8302  xrnemnf  8449  xrnepnf  8450  mnfltxr  8457  nn0pnfge0  8462  elfzonlteqm1  8816  m1expcl2  8911  bj-nn0suc  9394  bj-inf2vnlem2  9401  bj-nn0sucALT  9408