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  2910  eueq3dc  2911  sbcor  3007  elun  3276  ssun  3314  inss  3365  undif3ss  3396  ifsbdc  3546  ifiddc  3568  eqifdc  3569  ifnotdc  3571  ifandc  3572  ifordc  3573  elpr2  3614  sssnr  3753  ssprr  3756  sstpr  3757  preq12b  3770  exmidn0m  4201  copsexg  4244  sotritric  4324  regexmidlem1  4532  nn0eln0  4619  xpeq0r  5051  funtpg  5267  acexmidlemcase  5869  acexmidlem2  5871  el2oss1o  6443  nnm00  6530  djuss  7068  eldju2ndl  7070  eldju2ndr  7071  updjud  7080  nnnninf2  7124  exmidonfinlem  7191  exmidfodomrlemim  7199  exmidaclem  7206  renfdisj  8016  sup3exmid  8913  nn0ge0  9200  elnnnn0b  9219  xnn0xr  9243  xnn0nemnf  9249  elnn0z  9265  nn0n0n1ge2b  9331  nn0le2is012  9334  nn0ind-raph  9369  uzin  9559  elnn1uz2  9606  indstr2  9608  nn0ledivnn  9766  xrnemnf  9776  xrnepnf  9777  mnfltxr  9785  nn0pnfge0  9790  xnn0lenn0nn0  9864  xnn0xadd0  9866  elfzonlteqm1  10209  fldiv4p1lem1div2  10304  flqeqceilz  10317  modfzo0difsn  10394  m1expcl2  10541  m1expeven  10566  facp1  10709  faclbnd3  10722  bcn1  10737  hashinfuni  10756  hashfzp1  10803  isumz  11396  arisum  11505  arisum2  11506  ntrivcvgap  11555  prod1dc  11593  fprodfac  11622  mulsucdiv2z  11889  nn0o1gt2  11909  nno  11910  nn0o  11911  dfgcd2  12014  mulgcd  12016  gcdmultiplez  12021  dvdssq  12031  cncongr2  12103  prm2orodd  12125  dfphi2  12219  nnnn0modprm0  12254  prm23lt5  12262  pcmptcl  12339  oddprmdvds  12351  recnprss  14126  dvexp2  14146  coseq0negpitopi  14227  lgslem4  14374  2lgsoddprmlem3  14429  bj-dcstab  14478  bj-nn0suc  14686  bj-inf2vnlem2  14693  bj-nn0sucALT  14700  012of  14715  2o01f  14716