Theorem jaoi 716

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

Syntax hints:   -> wi 4   \/ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  717  jaoa  720  imorr  721  pm2.53  722  pm1.4  727  imorri  749  ioran  752  pm3.14  753  pm1.2  756  orim12i  759  pm1.5  765  pm2.41  776  pm2.42  777  pm2.4  778  pm4.44  779  pm4.78i  782  jaoian  795  jao1i  796  pm2.64  801  pm2.76  808  pm2.82  812  pm3.2ni  813  andi  818  dcim  841  condcOLD  854  pm2.61ddc  861  pm5.18dc  883  pm2.85dc  905  peircedc  914  dcan  933  dcor  935  pm4.42r  971  oplem1  975  xoranor  1377  biassdc  1395  anxordi  1400  19.33  1484  hbequid  1513  hbor  1546  19.30dc  1627  19.43  1628  19.32r  1680  hbae  1718  equvini  1758  equveli  1759  exdistrfor  1800  dveeq2  1815  dveeq2or  1816  sbequi  1839  nfsbxy  1942  nfsbxyt  1943  sbcomxyyz  1972  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  modc  2069  mooran1  2098  moexexdc  2110  rgen2a  2531  r19.32r  2623  eueq2dc  2912  eueq3dc  2913  sbcor  3009  elun  3278  ssun  3316  inss  3367  undif3ss  3398  ifsbdc  3548  ifiddc  3570  eqifdc  3571  ifnotdc  3573  ifandc  3574  ifordc  3575  elpr2  3616  sssnr  3755  ssprr  3758  sstpr  3759  preq12b  3772  exmidn0m  4203  copsexg  4246  sotritric  4326  regexmidlem1  4534  nn0eln0  4621  xpeq0r  5053  funtpg  5269  acexmidlemcase  5873  acexmidlem2  5875  el2oss1o  6447  nnm00  6534  djuss  7072  eldju2ndl  7074  eldju2ndr  7075  updjud  7084  nnnninf2  7128  exmidonfinlem  7195  exmidfodomrlemim  7203  exmidaclem  7210  renfdisj  8020  sup3exmid  8917  nn0ge0  9204  elnnnn0b  9223  xnn0xr  9247  xnn0nemnf  9253  elnn0z  9269  nn0n0n1ge2b  9335  nn0le2is012  9338  nn0ind-raph  9373  uzin  9563  elnn1uz2  9610  indstr2  9612  nn0ledivnn  9770  xrnemnf  9780  xrnepnf  9781  mnfltxr  9789  nn0pnfge0  9794  xnn0lenn0nn0  9868  xnn0xadd0  9870  elfzonlteqm1  10213  fldiv4p1lem1div2  10308  flqeqceilz  10321  modfzo0difsn  10398  m1expcl2  10545  m1expeven  10570  facp1  10713  faclbnd3  10726  bcn1  10741  hashinfuni  10760  hashfzp1  10807  isumz  11400  arisum  11509  arisum2  11510  ntrivcvgap  11559  prod1dc  11597  fprodfac  11626  mulsucdiv2z  11893  nn0o1gt2  11913  nno  11914  nn0o  11915  dfgcd2  12018  mulgcd  12020  gcdmultiplez  12025  dvdssq  12035  cncongr2  12107  prm2orodd  12129  dfphi2  12223  nnnn0modprm0  12258  prm23lt5  12266  pcmptcl  12343  oddprmdvds  12355  recnprss  14344  dvexp2  14364  coseq0negpitopi  14445  lgslem4  14592  2lgsoddprmlem3  14647  bj-dcstab  14696  bj-nn0suc  14904  bj-inf2vnlem2  14911  bj-nn0sucALT  14918  012of  14934  2o01f  14935