Theorem jaoi 706

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

Syntax hints:   -> wi 4   \/ wo 698

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  jaod  707  jaoa  710  imorr  711  pm2.53  712  pm1.4  717  imorri  739  ioran  742  pm3.14  743  pm1.2  746  orim12i  749  pm1.5  755  pm2.41  766  pm2.42  767  pm2.4  768  pm4.44  769  pm4.78i  772  jaoian  785  jao1i  786  pm2.64  791  pm2.76  798  pm2.82  802  pm3.2ni  803  andi  808  dcim  831  condcOLD  844  pm2.61ddc  851  pm5.18dc  873  pm2.85dc  895  peircedc  904  dcan  923  dcor  925  pm4.42r  961  oplem1  965  xoranor  1367  biassdc  1385  anxordi  1390  19.33  1472  hbequid  1501  hbor  1534  19.30dc  1615  19.43  1616  19.32r  1668  hbae  1706  equvini  1746  equveli  1747  exdistrfor  1788  dveeq2  1803  dveeq2or  1804  sbequi  1827  nfsbxy  1930  nfsbxyt  1931  sbcomxyyz  1960  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  modc  2057  mooran1  2086  moexexdc  2098  rgen2a  2519  r19.32r  2611  eueq2dc  2898  eueq3dc  2899  sbcor  2994  elun  3262  ssun  3300  inss  3351  undif3ss  3382  ifsbdc  3531  ifiddc  3552  eqifdc  3553  ifnotdc  3555  ifandc  3556  elpr2  3597  sssnr  3732  ssprr  3735  sstpr  3736  preq12b  3749  exmidn0m  4179  copsexg  4221  sotritric  4301  regexmidlem1  4509  nn0eln0  4596  xpeq0r  5025  funtpg  5238  acexmidlemcase  5836  acexmidlem2  5838  el2oss1o  6407  nnm00  6493  djuss  7031  eldju2ndl  7033  eldju2ndr  7034  updjud  7043  nnnninf2  7087  exmidonfinlem  7145  exmidfodomrlemim  7153  exmidaclem  7160  renfdisj  7954  sup3exmid  8848  nn0ge0  9135  elnnnn0b  9154  xnn0xr  9178  xnn0nemnf  9184  elnn0z  9200  nn0n0n1ge2b  9266  nn0le2is012  9269  nn0ind-raph  9304  uzin  9494  elnn1uz2  9541  indstr2  9543  nn0ledivnn  9699  xrnemnf  9709  xrnepnf  9710  mnfltxr  9718  nn0pnfge0  9723  xnn0lenn0nn0  9797  xnn0xadd0  9799  elfzonlteqm1  10141  fldiv4p1lem1div2  10236  flqeqceilz  10249  modfzo0difsn  10326  m1expcl2  10473  m1expeven  10498  facp1  10639  faclbnd3  10652  bcn1  10667  hashinfuni  10686  hashfzp1  10733  isumz  11326  arisum  11435  arisum2  11436  ntrivcvgap  11485  prod1dc  11523  fprodfac  11552  mulsucdiv2z  11818  nn0o1gt2  11838  nno  11839  nn0o  11840  dfgcd2  11943  mulgcd  11945  gcdmultiplez  11950  dvdssq  11960  cncongr2  12032  prm2orodd  12054  dfphi2  12148  nnnn0modprm0  12183  prm23lt5  12191  pcmptcl  12268  oddprmdvds  12280  recnprss  13256  dvexp2  13276  coseq0negpitopi  13357  lgslem4  13504  bj-dcstab  13597  bj-nn0suc  13806  bj-inf2vnlem2  13813  bj-nn0sucALT  13820  012of  13835  2o01f  13836