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  1508  hbequid  1537  hbor  1570  19.30dc  1651  19.43  1652  19.32r  1704  hbae  1742  equvini  1782  equveli  1783  exdistrfor  1824  dveeq2  1839  dveeq2or  1840  sbequi  1863  nfsbxy  1971  nfsbxyt  1972  sbcomxyyz  2001  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  modc  2099  mooran1  2128  moexexdc  2140  rgen2a  2562  r19.32r  2654  eueq2dc  2953  eueq3dc  2954  sbcor  3050  elun  3322  ssun  3360  inss  3411  undif3ss  3442  elif  3591  ifsbdc  3592  ifiddc  3615  eqifdc  3616  ifnotdc  3618  ifandc  3620  ifordc  3621  elpr2  3665  sssnr  3807  ssprr  3810  sstpr  3811  preq12b  3824  elpr2elpr  3830  exmidn0m  4261  copsexg  4306  sotritric  4389  regexmidlem1  4599  nn0eln0  4686  xpeq0r  5124  funtpg  5344  acexmidlemcase  5962  acexmidlem2  5964  el2oss1o  6552  nnm00  6639  djuss  7198  eldju2ndl  7200  eldju2ndr  7201  updjud  7210  nnnninf2  7255  exmidonfinlem  7332  exmidfodomrlemim  7340  exmidaclem  7351  renfdisj  8167  sup3exmid  9065  nn0ge0  9355  elnnnn0b  9374  xnn0xr  9398  xnn0nemnf  9404  elnn0z  9420  nn0n0n1ge2b  9487  nn0le2is012  9490  nn0ind-raph  9525  uzin  9716  elnn1uz2  9763  indstr2  9765  nn0ledivnn  9924  xrnemnf  9934  xrnepnf  9935  mnfltxr  9943  nn0pnfge0  9948  xnn0lenn0nn0  10022  xnn0xadd0  10024  elfzonlteqm1  10376  xqltnle  10447  fldiv4p1lem1div2  10485  fldiv4lem1div2  10487  flqeqceilz  10500  modfzo0difsn  10577  m1expcl2  10743  m1expeven  10768  zzlesq  10890  facp1  10912  faclbnd3  10925  bcn1  10940  hashinfuni  10959  hashfzp1  11006  swrdnd  11150  pfxccatin12  11224  swrdccat  11226  pfxccat3a  11229  isumz  11815  arisum  11924  arisum2  11925  ntrivcvgap  11974  prod1dc  12012  fprodfac  12041  mulsucdiv2z  12311  nn0o1gt2  12331  nno  12332  nn0o  12333  dfgcd2  12450  mulgcd  12452  gcdmultiplez  12457  dvdssq  12467  cncongr2  12541  prm2orodd  12563  dfphi2  12657  nnnn0modprm0  12693  prm23lt5  12701  pcmptcl  12780  oddprmdvds  12792  4sqlem19  12847  mulgnn0gsum  13579  recnprss  15274  dvexp2  15299  dvmptid  15303  coseq0negpitopi  15423  lgslem4  15595  gausslemma2dlem0i  15649  lgsquadlem2  15670  2lgslem3  15693  2lgs  15696  2lgsoddprmlem3  15703  upgrm  15811  upgrfi  15813  upgrex  15814  upgruhgr  15822  bj-dcstab  15892  bj-nn0suc  16099  bj-inf2vnlem2  16106  bj-nn0sucALT  16113  012of  16130  2o01f  16131