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  2911  eueq3dc  2912  sbcor  3008  elun  3277  ssun  3315  inss  3366  undif3ss  3397  ifsbdc  3547  ifiddc  3569  eqifdc  3570  ifnotdc  3572  ifandc  3573  ifordc  3574  elpr2  3615  sssnr  3754  ssprr  3757  sstpr  3758  preq12b  3771  exmidn0m  4202  copsexg  4245  sotritric  4325  regexmidlem1  4533  nn0eln0  4620  xpeq0r  5052  funtpg  5268  acexmidlemcase  5870  acexmidlem2  5872  el2oss1o  6444  nnm00  6531  djuss  7069  eldju2ndl  7071  eldju2ndr  7072  updjud  7081  nnnninf2  7125  exmidonfinlem  7192  exmidfodomrlemim  7200  exmidaclem  7207  renfdisj  8017  sup3exmid  8914  nn0ge0  9201  elnnnn0b  9220  xnn0xr  9244  xnn0nemnf  9250  elnn0z  9266  nn0n0n1ge2b  9332  nn0le2is012  9335  nn0ind-raph  9370  uzin  9560  elnn1uz2  9607  indstr2  9609  nn0ledivnn  9767  xrnemnf  9777  xrnepnf  9778  mnfltxr  9786  nn0pnfge0  9791  xnn0lenn0nn0  9865  xnn0xadd0  9867  elfzonlteqm1  10210  fldiv4p1lem1div2  10305  flqeqceilz  10318  modfzo0difsn  10395  m1expcl2  10542  m1expeven  10567  facp1  10710  faclbnd3  10723  bcn1  10738  hashinfuni  10757  hashfzp1  10804  isumz  11397  arisum  11506  arisum2  11507  ntrivcvgap  11556  prod1dc  11594  fprodfac  11623  mulsucdiv2z  11890  nn0o1gt2  11910  nno  11911  nn0o  11912  dfgcd2  12015  mulgcd  12017  gcdmultiplez  12022  dvdssq  12032  cncongr2  12104  prm2orodd  12126  dfphi2  12220  nnnn0modprm0  12255  prm23lt5  12263  pcmptcl  12340  oddprmdvds  12352  recnprss  14159  dvexp2  14179  coseq0negpitopi  14260  lgslem4  14407  2lgsoddprmlem3  14462  bj-dcstab  14511  bj-nn0suc  14719  bj-inf2vnlem2  14726  bj-nn0sucALT  14733  012of  14748  2o01f  14749