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  827  condcOLD  840  pm2.61ddc  847  pm5.18dc  869  pm2.85dc  891  peircedc  900  dcan  919  dcor  920  pm4.42r  956  oplem1  960  xoranor  1356  biassdc  1374  anxordi  1379  19.33  1461  hbequid  1490  hbor  1523  19.30dc  1604  19.43  1605  19.32r  1657  hbae  1695  equvini  1735  equveli  1736  exdistrfor  1777  dveeq2  1792  dveeq2or  1793  sbequi  1816  nfsbxy  1919  nfsbxyt  1920  sbcomxyyz  1949  dvelimALT  1987  dvelimfv  1988  dvelimor  1995  modc  2046  mooran1  2075  moexexdc  2087  rgen2a  2508  r19.32r  2600  eueq2dc  2881  eueq3dc  2882  sbcor  2977  elun  3244  ssun  3282  inss  3333  undif3ss  3364  ifsbdc  3513  ifiddc  3534  eqifdc  3535  ifandc  3537  elpr2  3578  sssnr  3712  ssprr  3715  sstpr  3716  preq12b  3729  exmidn0m  4157  copsexg  4199  sotritric  4279  regexmidlem1  4486  nn0eln0  4573  xpeq0r  5001  funtpg  5214  acexmidlemcase  5809  acexmidlem2  5811  nnm00  6465  djuss  7000  eldju2ndl  7002  eldju2ndr  7003  updjud  7012  nnnninf2  7055  exmidonfinlem  7107  exmidfodomrlemim  7115  exmidaclem  7122  renfdisj  7916  sup3exmid  8807  nn0ge0  9094  elnnnn0b  9113  xnn0xr  9137  xnn0nemnf  9143  elnn0z  9159  nn0n0n1ge2b  9222  nn0le2is012  9225  nn0ind-raph  9260  uzin  9450  elnn1uz2  9496  indstr2  9498  nn0ledivnn  9652  xrnemnf  9662  xrnepnf  9663  mnfltxr  9671  nn0pnfge0  9676  xnn0lenn0nn0  9747  xnn0xadd0  9749  elfzonlteqm1  10087  fldiv4p1lem1div2  10182  flqeqceilz  10195  modfzo0difsn  10272  m1expcl2  10419  m1expeven  10444  facp1  10581  faclbnd3  10594  bcn1  10609  hashinfuni  10628  hashfzp1  10675  isumz  11263  arisum  11372  arisum2  11373  ntrivcvgap  11422  prod1dc  11460  fprodfac  11489  mulsucdiv2z  11749  nn0o1gt2  11769  nno  11770  nn0o  11771  dfgcd2  11869  mulgcd  11871  gcdmultiplez  11876  dvdssq  11886  cncongr2  11952  prm2orodd  11974  dfphi2  12063  recnprss  12995  dvexp2  13015  coseq0negpitopi  13096  bj-dcstab  13266  bj-nn0suc  13477  bj-inf2vnlem2  13484  bj-nn0sucALT  13491  el2oss1o  13503  012of  13506  2o01f  13507