Theorem jaoi 724

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

Syntax hints:   -> wi 4   \/ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  725  jaoa  728  imorr  729  pm2.53  730  pm1.4  735  imorri  757  ioran  760  pm3.14  761  pm1.2  764  orim12i  767  pm1.5  773  pm2.41  784  pm2.42  785  pm2.4  786  pm4.44  787  pm4.78i  790  jaoian  803  jao1i  804  pm2.64  809  pm2.76  816  pm2.82  820  pm3.2ni  821  andi  826  dcim  849  condcOLD  862  pm2.61ddc  869  pm5.18dc  891  pm2.85dc  913  peircedc  922  dcor  944  pm4.42r  980  oplem1  984  ifp2  989  ifpiddc  1000  1fpid3  1003  xoranor  1422  biassdc  1440  anxordi  1445  19.33  1533  hbequid  1562  hbor  1595  19.30dc  1676  19.43  1677  19.32r  1728  hbae  1766  equvini  1807  equveli  1808  exdistrfor  1849  dveeq2  1864  dveeq2or  1865  sbequi  1888  nfsbxy  1996  nfsbxyt  1997  sbcomxyyz  2026  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  modc  2124  mooran1  2153  moexexdc  2165  rgen2a  2596  r19.32r  2689  eueq2dc  2990  eueq3dc  2991  sbcor  3087  elun  3360  ssun  3398  inss  3451  undif3ss  3482  elif  3634  ifsbdc  3635  ifiddc  3658  eqifdc  3659  ifnotdc  3661  ifandc  3663  ifordc  3664  elpr2  3711  rabsnifsb  3757  sssnr  3857  ssprr  3860  sstpr  3861  preq12b  3874  elpr2elpr  3880  exmidn0m  4314  copsexg  4360  sotritric  4445  regexmidlem1  4655  nn0eln0  4742  xpeq0r  5185  funtpg  5407  acexmidlemcase  6045  acexmidlem2  6047  el2oss1o  6676  nnm00  6763  djuss  7361  eldju2ndl  7363  eldju2ndr  7364  updjud  7373  nnnninf2  7418  sspw1or2  7495  exmidonfinlem  7496  exmidfodomrlemim  7504  exmidaclem  7515  renfdisj  8333  sup3exmid  9231  nn0ge0  9521  elnnnn0b  9540  xnn0xr  9568  xnn0nemnf  9574  elnn0z  9590  nn0n0n1ge2b  9657  nn0le2is012  9660  nn0ind-raph  9695  uzin  9887  elnn1uz2  9939  indstr2  9941  nn0ledivnn  10100  xrnemnf  10110  xrnepnf  10111  mnfltxr  10119  nn0pnfge0  10124  xnn0lenn0nn0  10198  xnn0xadd0  10200  elfzonlteqm1  10555  xqltnle  10627  fldiv4p1lem1div2  10665  fldiv4lem1div2  10667  flqeqceilz  10680  modfzo0difsn  10757  m1expcl2  10923  m1expeven  10948  zzlesq  11070  facp1  11092  faclbnd3  11105  bcn1  11120  hashinfuni  11140  hashfzp1  11189  swrdnd  11351  pfxccatin12  11425  swrdccat  11427  pfxccat3a  11430  isumz  12075  arisum  12184  arisum2  12185  ntrivcvgap  12234  prod1dc  12272  fprodfac  12301  mulsucdiv2z  12571  nn0o1gt2  12591  nno  12592  nn0o  12593  dfgcd2  12710  mulgcd  12712  gcdmultiplez  12717  dvdssq  12727  cncongr2  12801  prm2orodd  12823  dfphi2  12917  nnnn0modprm0  12953  prm23lt5  12961  pcmptcl  13040  oddprmdvds  13052  4sqlem19  13107  mulgnn0gsum  13845  recnprss  15552  dvexp2  15577  dvmptid  15581  coseq0negpitopi  15701  lgslem4  15876  gausslemma2dlem0i  15930  lgsquadlem2  15951  2lgslem3  15974  2lgs  15977  2lgsoddprmlem3  15984  upgrm  16095  upgrfi  16097  upgrex  16098  upgruhgr  16106  uspgrushgr  16175  uhgr2edg  16201  usgredg4  16210  upgriswlkdc  16355  umgrclwwlkge2  16397  eupth2lem3lem4fi  16468  konigsberg  16488  bj-dcstab  16528  bj-nn0suc  16734  bj-inf2vnlem2  16741  bj-nn0sucALT  16748  012of  16767  2o01f  16768