Theorem jaoi 718

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

Syntax hints:   -> wi 4   \/ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  719  jaoa  722  imorr  723  pm2.53  724  pm1.4  729  imorri  751  ioran  754  pm3.14  755  pm1.2  758  orim12i  761  pm1.5  767  pm2.41  778  pm2.42  779  pm2.4  780  pm4.44  781  pm4.78i  784  jaoian  797  jao1i  798  pm2.64  803  pm2.76  810  pm2.82  814  pm3.2ni  815  andi  820  dcim  843  condcOLD  856  pm2.61ddc  863  pm5.18dc  885  pm2.85dc  907  peircedc  916  dcor  938  pm4.42r  974  oplem1  978  xoranor  1397  biassdc  1415  anxordi  1420  19.33  1507  hbequid  1536  hbor  1569  19.30dc  1650  19.43  1651  19.32r  1703  hbae  1741  equvini  1781  equveli  1782  exdistrfor  1823  dveeq2  1838  dveeq2or  1839  sbequi  1862  nfsbxy  1970  nfsbxyt  1971  sbcomxyyz  2000  dvelimALT  2038  dvelimfv  2039  dvelimor  2046  modc  2097  mooran1  2126  moexexdc  2138  rgen2a  2560  r19.32r  2652  eueq2dc  2946  eueq3dc  2947  sbcor  3043  elun  3314  ssun  3352  inss  3403  undif3ss  3434  ifsbdc  3583  ifiddc  3606  eqifdc  3607  ifnotdc  3609  ifandc  3610  ifordc  3611  elpr2  3655  sssnr  3794  ssprr  3797  sstpr  3798  preq12b  3811  exmidn0m  4245  copsexg  4288  sotritric  4371  regexmidlem1  4581  nn0eln0  4668  xpeq0r  5105  funtpg  5325  acexmidlemcase  5939  acexmidlem2  5941  el2oss1o  6529  nnm00  6616  djuss  7172  eldju2ndl  7174  eldju2ndr  7175  updjud  7184  nnnninf2  7229  exmidonfinlem  7301  exmidfodomrlemim  7309  exmidaclem  7320  renfdisj  8132  sup3exmid  9030  nn0ge0  9320  elnnnn0b  9339  xnn0xr  9363  xnn0nemnf  9369  elnn0z  9385  nn0n0n1ge2b  9452  nn0le2is012  9455  nn0ind-raph  9490  uzin  9681  elnn1uz2  9728  indstr2  9730  nn0ledivnn  9889  xrnemnf  9899  xrnepnf  9900  mnfltxr  9908  nn0pnfge0  9913  xnn0lenn0nn0  9987  xnn0xadd0  9989  elfzonlteqm1  10339  xqltnle  10410  fldiv4p1lem1div2  10448  fldiv4lem1div2  10450  flqeqceilz  10463  modfzo0difsn  10540  m1expcl2  10706  m1expeven  10731  zzlesq  10853  facp1  10875  faclbnd3  10888  bcn1  10903  hashinfuni  10922  hashfzp1  10969  swrdnd  11112  isumz  11700  arisum  11809  arisum2  11810  ntrivcvgap  11859  prod1dc  11897  fprodfac  11926  mulsucdiv2z  12196  nn0o1gt2  12216  nno  12217  nn0o  12218  dfgcd2  12335  mulgcd  12337  gcdmultiplez  12342  dvdssq  12352  cncongr2  12426  prm2orodd  12448  dfphi2  12542  nnnn0modprm0  12578  prm23lt5  12586  pcmptcl  12665  oddprmdvds  12677  4sqlem19  12732  mulgnn0gsum  13464  recnprss  15159  dvexp2  15184  dvmptid  15188  coseq0negpitopi  15308  lgslem4  15480  gausslemma2dlem0i  15534  lgsquadlem2  15555  2lgslem3  15578  2lgs  15581  2lgsoddprmlem3  15588  bj-dcstab  15696  bj-nn0suc  15904  bj-inf2vnlem2  15911  bj-nn0sucALT  15918  012of  15934  2o01f  15935