Theorem jaoi 688

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 687	. 2 |- ( ( ( ph -> ps ) /\ ( ch -> ps ) ) -> ( ( ph \/ ch ) -> ps ) )
4	1, 2, 3	mp2an 420	1 |- ( ( ph \/ ch ) -> ps )

Syntax hints:   -> wi 4   \/ wo 680

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  jaod  689  jaoa  692  imorr  693  pm2.53  694  pm1.4  699  imorri  721  ioran  724  pm3.14  725  pm1.2  728  orim12i  731  pm1.5  737  pm2.41  748  pm2.42  749  pm2.4  750  pm4.44  751  pm4.78i  754  jaoian  767  jao1i  768  pm2.64  773  pm2.76  780  pm2.82  784  pm3.2ni  785  andi  790  dcim  809  condcOLD  822  pm2.61ddc  829  pm5.18dc  851  pm2.85dc  873  peircedc  882  dcan  901  dcor  902  pm4.42r  938  oplem1  942  xoranor  1338  biassdc  1356  anxordi  1361  19.33  1443  hbequid  1476  hbor  1508  19.30dc  1589  19.43  1590  19.32r  1641  hbae  1679  equvini  1714  equveli  1715  exdistrfor  1754  dveeq2  1769  dveeq2or  1770  sbequi  1793  nfsbxy  1893  nfsbxyt  1894  sbcomxyyz  1921  dvelimALT  1961  dvelimfv  1962  dvelimor  1969  modc  2018  mooran1  2047  moexexdc  2059  rgen2a  2460  r19.32r  2552  eueq2dc  2826  eueq3dc  2827  sbcor  2921  elun  3183  ssun  3221  inss  3272  undif3ss  3303  ifsbdc  3452  ifiddc  3471  eqifdc  3472  ifandc  3474  elpr2  3515  sssnr  3646  ssprr  3649  sstpr  3650  preq12b  3663  exmidn0m  4084  copsexg  4126  sotritric  4206  regexmidlem1  4408  nn0eln0  4493  xpeq0r  4919  funtpg  5132  acexmidlemcase  5723  acexmidlem2  5725  nnm00  6379  djuss  6907  eldju2ndl  6909  eldju2ndr  6910  updjud  6919  exmidfodomrlemim  7005  exmidaclem  7012  renfdisj  7748  sup3exmid  8625  nn0ge0  8906  elnnnn0b  8925  xnn0xr  8949  xnn0nemnf  8955  elnn0z  8971  nn0n0n1ge2b  9034  nn0le2is012  9037  nn0ind-raph  9072  uzin  9260  elnn1uz2  9303  indstr2  9305  nn0ledivnn  9447  xrnemnf  9457  xrnepnf  9458  mnfltxr  9465  nn0pnfge0  9470  xnn0lenn0nn0  9541  xnn0xadd0  9543  elfzonlteqm1  9880  fldiv4p1lem1div2  9971  flqeqceilz  9984  modfzo0difsn  10061  m1expcl2  10208  m1expeven  10233  facp1  10369  faclbnd3  10382  bcn1  10397  hashinfuni  10416  hashfzp1  10463  isumz  11050  arisum  11159  arisum2  11160  mulsucdiv2z  11430  nn0o1gt2  11450  nno  11451  nn0o  11452  dfgcd2  11548  mulgcd  11550  gcdmultiplez  11555  dvdssq  11565  cncongr2  11631  prm2orodd  11653  dfphi2  11741  recnprss  12611  bj-dcstab  12654  bj-nn0suc  12854  bj-inf2vnlem2  12861  bj-nn0sucALT  12868  el2oss1o  12880  isomninnlem  12917