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  4246  copsexg  4289  sotritric  4372  regexmidlem1  4582  nn0eln0  4669  xpeq0r  5106  funtpg  5326  acexmidlemcase  5941  acexmidlem2  5943  el2oss1o  6531  nnm00  6618  djuss  7174  eldju2ndl  7176  eldju2ndr  7177  updjud  7186  nnnninf2  7231  exmidonfinlem  7303  exmidfodomrlemim  7311  exmidaclem  7322  renfdisj  8134  sup3exmid  9032  nn0ge0  9322  elnnnn0b  9341  xnn0xr  9365  xnn0nemnf  9371  elnn0z  9387  nn0n0n1ge2b  9454  nn0le2is012  9457  nn0ind-raph  9492  uzin  9683  elnn1uz2  9730  indstr2  9732  nn0ledivnn  9891  xrnemnf  9901  xrnepnf  9902  mnfltxr  9910  nn0pnfge0  9915  xnn0lenn0nn0  9989  xnn0xadd0  9991  elfzonlteqm1  10341  xqltnle  10412  fldiv4p1lem1div2  10450  fldiv4lem1div2  10452  flqeqceilz  10465  modfzo0difsn  10542  m1expcl2  10708  m1expeven  10733  zzlesq  10855  facp1  10877  faclbnd3  10890  bcn1  10905  hashinfuni  10924  hashfzp1  10971  swrdnd  11115  isumz  11733  arisum  11842  arisum2  11843  ntrivcvgap  11892  prod1dc  11930  fprodfac  11959  mulsucdiv2z  12229  nn0o1gt2  12249  nno  12250  nn0o  12251  dfgcd2  12368  mulgcd  12370  gcdmultiplez  12375  dvdssq  12385  cncongr2  12459  prm2orodd  12481  dfphi2  12575  nnnn0modprm0  12611  prm23lt5  12619  pcmptcl  12698  oddprmdvds  12710  4sqlem19  12765  mulgnn0gsum  13497  recnprss  15192  dvexp2  15217  dvmptid  15221  coseq0negpitopi  15341  lgslem4  15513  gausslemma2dlem0i  15567  lgsquadlem2  15588  2lgslem3  15611  2lgs  15614  2lgsoddprmlem3  15621  bj-dcstab  15729  bj-nn0suc  15937  bj-inf2vnlem2  15944  bj-nn0sucALT  15951  012of  15967  2o01f  15968