Theorem jaoi 717

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

Syntax hints:   -> wi 4   \/ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  718  jaoa  721  imorr  722  pm2.53  723  pm1.4  728  imorri  750  ioran  753  pm3.14  754  pm1.2  757  orim12i  760  pm1.5  766  pm2.41  777  pm2.42  778  pm2.4  779  pm4.44  780  pm4.78i  783  jaoian  796  jao1i  797  pm2.64  802  pm2.76  809  pm2.82  813  pm3.2ni  814  andi  819  dcim  842  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.85dc  906  peircedc  915  dcor  937  pm4.42r  973  oplem1  977  xoranor  1388  biassdc  1406  anxordi  1411  19.33  1495  hbequid  1524  hbor  1557  19.30dc  1638  19.43  1639  19.32r  1691  hbae  1729  equvini  1769  equveli  1770  exdistrfor  1811  dveeq2  1826  dveeq2or  1827  sbequi  1850  nfsbxy  1958  nfsbxyt  1959  sbcomxyyz  1988  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  modc  2085  mooran1  2114  moexexdc  2126  rgen2a  2548  r19.32r  2640  eueq2dc  2934  eueq3dc  2935  sbcor  3031  elun  3301  ssun  3339  inss  3390  undif3ss  3421  ifsbdc  3570  ifiddc  3592  eqifdc  3593  ifnotdc  3595  ifandc  3596  ifordc  3597  elpr2  3641  sssnr  3780  ssprr  3783  sstpr  3784  preq12b  3797  exmidn0m  4231  copsexg  4274  sotritric  4356  regexmidlem1  4566  nn0eln0  4653  xpeq0r  5089  funtpg  5306  acexmidlemcase  5914  acexmidlem2  5916  el2oss1o  6498  nnm00  6585  djuss  7131  eldju2ndl  7133  eldju2ndr  7134  updjud  7143  nnnninf2  7188  exmidonfinlem  7255  exmidfodomrlemim  7263  exmidaclem  7270  renfdisj  8081  sup3exmid  8978  nn0ge0  9268  elnnnn0b  9287  xnn0xr  9311  xnn0nemnf  9317  elnn0z  9333  nn0n0n1ge2b  9399  nn0le2is012  9402  nn0ind-raph  9437  uzin  9628  elnn1uz2  9675  indstr2  9677  nn0ledivnn  9836  xrnemnf  9846  xrnepnf  9847  mnfltxr  9855  nn0pnfge0  9860  xnn0lenn0nn0  9934  xnn0xadd0  9936  elfzonlteqm1  10280  xqltnle  10339  fldiv4p1lem1div2  10377  fldiv4lem1div2  10379  flqeqceilz  10392  modfzo0difsn  10469  m1expcl2  10635  m1expeven  10660  zzlesq  10782  facp1  10804  faclbnd3  10817  bcn1  10832  hashinfuni  10851  hashfzp1  10898  isumz  11535  arisum  11644  arisum2  11645  ntrivcvgap  11694  prod1dc  11732  fprodfac  11761  mulsucdiv2z  12029  nn0o1gt2  12049  nno  12050  nn0o  12051  dfgcd2  12154  mulgcd  12156  gcdmultiplez  12161  dvdssq  12171  cncongr2  12245  prm2orodd  12267  dfphi2  12361  nnnn0modprm0  12396  prm23lt5  12404  pcmptcl  12483  oddprmdvds  12495  4sqlem19  12550  mulgnn0gsum  13201  recnprss  14866  dvexp2  14891  dvmptid  14895  coseq0negpitopi  15012  lgslem4  15160  gausslemma2dlem0i  15214  lgsquadlem2  15235  2lgslem3  15258  2lgs  15261  2lgsoddprmlem3  15268  bj-dcstab  15318  bj-nn0suc  15526  bj-inf2vnlem2  15533  bj-nn0sucALT  15540  012of  15556  2o01f  15557