Theorem jaoi 705

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

Syntax hints:   -> wi 4   \/ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  jaod  706  jaoa  709  imorr  710  pm2.53  711  pm1.4  716  imorri  738  ioran  741  pm3.14  742  pm1.2  745  orim12i  748  pm1.5  754  pm2.41  765  pm2.42  766  pm2.4  767  pm4.44  768  pm4.78i  771  jaoian  784  jao1i  785  pm2.64  790  pm2.76  797  pm2.82  801  pm3.2ni  802  andi  807  dcim  826  condcOLD  839  pm2.61ddc  846  pm5.18dc  868  pm2.85dc  890  peircedc  899  dcan  918  dcor  919  pm4.42r  955  oplem1  959  xoranor  1355  biassdc  1373  anxordi  1378  19.33  1460  hbequid  1493  hbor  1525  19.30dc  1606  19.43  1607  19.32r  1658  hbae  1696  equvini  1731  equveli  1732  exdistrfor  1772  dveeq2  1787  dveeq2or  1788  sbequi  1811  nfsbxy  1915  nfsbxyt  1916  sbcomxyyz  1945  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  modc  2042  mooran1  2071  moexexdc  2083  rgen2a  2486  r19.32r  2578  eueq2dc  2857  eueq3dc  2858  sbcor  2953  elun  3217  ssun  3255  inss  3306  undif3ss  3337  ifsbdc  3486  ifiddc  3505  eqifdc  3506  ifandc  3508  elpr2  3549  sssnr  3680  ssprr  3683  sstpr  3684  preq12b  3697  exmidn0m  4124  copsexg  4166  sotritric  4246  regexmidlem1  4448  nn0eln0  4533  xpeq0r  4961  funtpg  5174  acexmidlemcase  5769  acexmidlem2  5771  nnm00  6425  djuss  6955  eldju2ndl  6957  eldju2ndr  6958  updjud  6967  exmidonfinlem  7049  exmidfodomrlemim  7057  exmidaclem  7064  renfdisj  7824  sup3exmid  8715  nn0ge0  9002  elnnnn0b  9021  xnn0xr  9045  xnn0nemnf  9051  elnn0z  9067  nn0n0n1ge2b  9130  nn0le2is012  9133  nn0ind-raph  9168  uzin  9358  elnn1uz2  9401  indstr2  9403  nn0ledivnn  9554  xrnemnf  9564  xrnepnf  9565  mnfltxr  9572  nn0pnfge0  9577  xnn0lenn0nn0  9648  xnn0xadd0  9650  elfzonlteqm1  9987  fldiv4p1lem1div2  10078  flqeqceilz  10091  modfzo0difsn  10168  m1expcl2  10315  m1expeven  10340  facp1  10476  faclbnd3  10489  bcn1  10504  hashinfuni  10523  hashfzp1  10570  isumz  11158  arisum  11267  arisum2  11268  ntrivcvgap  11317  mulsucdiv2z  11582  nn0o1gt2  11602  nno  11603  nn0o  11604  dfgcd2  11702  mulgcd  11704  gcdmultiplez  11709  dvdssq  11719  cncongr2  11785  prm2orodd  11807  dfphi2  11896  recnprss  12825  dvexp2  12845  coseq0negpitopi  12917  bj-dcstab  12961  bj-nn0suc  13162  bj-inf2vnlem2  13169  bj-nn0sucALT  13176  el2oss1o  13188  isomninnlem  13225