Theorem jaoi 721

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

Syntax hints:   -> wi 4   \/ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  722  jaoa  725  imorr  726  pm2.53  727  pm1.4  732  imorri  754  ioran  757  pm3.14  758  pm1.2  761  orim12i  764  pm1.5  770  pm2.41  781  pm2.42  782  pm2.4  783  pm4.44  784  pm4.78i  787  jaoian  800  jao1i  801  pm2.64  806  pm2.76  813  pm2.82  817  pm3.2ni  818  andi  823  dcim  846  condcOLD  859  pm2.61ddc  866  pm5.18dc  888  pm2.85dc  910  peircedc  919  dcor  941  pm4.42r  977  oplem1  981  ifp2  986  ifpiddc  997  1fpid3  1000  xoranor  1419  biassdc  1437  anxordi  1442  19.33  1530  hbequid  1559  hbor  1592  19.30dc  1673  19.43  1674  19.32r  1726  hbae  1764  equvini  1804  equveli  1805  exdistrfor  1846  dveeq2  1861  dveeq2or  1862  sbequi  1885  nfsbxy  1993  nfsbxyt  1994  sbcomxyyz  2023  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  modc  2121  mooran1  2150  moexexdc  2162  rgen2a  2584  r19.32r  2677  eueq2dc  2976  eueq3dc  2977  sbcor  3073  elun  3345  ssun  3383  inss  3434  undif3ss  3465  elif  3614  ifsbdc  3615  ifiddc  3638  eqifdc  3639  ifnotdc  3641  ifandc  3643  ifordc  3644  elpr2  3688  sssnr  3831  ssprr  3834  sstpr  3835  preq12b  3848  elpr2elpr  3854  exmidn0m  4285  copsexg  4330  sotritric  4415  regexmidlem1  4625  nn0eln0  4712  xpeq0r  5151  funtpg  5372  acexmidlemcase  5996  acexmidlem2  5998  el2oss1o  6589  nnm00  6676  djuss  7237  eldju2ndl  7239  eldju2ndr  7240  updjud  7249  nnnninf2  7294  exmidonfinlem  7371  exmidfodomrlemim  7379  exmidaclem  7390  renfdisj  8206  sup3exmid  9104  nn0ge0  9394  elnnnn0b  9413  xnn0xr  9437  xnn0nemnf  9443  elnn0z  9459  nn0n0n1ge2b  9526  nn0le2is012  9529  nn0ind-raph  9564  uzin  9755  elnn1uz2  9802  indstr2  9804  nn0ledivnn  9963  xrnemnf  9973  xrnepnf  9974  mnfltxr  9982  nn0pnfge0  9987  xnn0lenn0nn0  10061  xnn0xadd0  10063  elfzonlteqm1  10416  xqltnle  10487  fldiv4p1lem1div2  10525  fldiv4lem1div2  10527  flqeqceilz  10540  modfzo0difsn  10617  m1expcl2  10783  m1expeven  10808  zzlesq  10930  facp1  10952  faclbnd3  10965  bcn1  10980  hashinfuni  10999  hashfzp1  11046  swrdnd  11191  pfxccatin12  11265  swrdccat  11267  pfxccat3a  11270  isumz  11900  arisum  12009  arisum2  12010  ntrivcvgap  12059  prod1dc  12097  fprodfac  12126  mulsucdiv2z  12396  nn0o1gt2  12416  nno  12417  nn0o  12418  dfgcd2  12535  mulgcd  12537  gcdmultiplez  12542  dvdssq  12552  cncongr2  12626  prm2orodd  12648  dfphi2  12742  nnnn0modprm0  12778  prm23lt5  12786  pcmptcl  12865  oddprmdvds  12877  4sqlem19  12932  mulgnn0gsum  13665  recnprss  15361  dvexp2  15386  dvmptid  15390  coseq0negpitopi  15510  lgslem4  15682  gausslemma2dlem0i  15736  lgsquadlem2  15757  2lgslem3  15780  2lgs  15783  2lgsoddprmlem3  15790  upgrm  15900  upgrfi  15902  upgrex  15903  upgruhgr  15911  uspgrushgr  15978  uhgr2edg  16004  usgredg4  16013  upgriswlkdc  16071  bj-dcstab  16120  bj-nn0suc  16327  bj-inf2vnlem2  16334  bj-nn0sucALT  16341  012of  16357  2o01f  16358