Theorem jaoi 724

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

Syntax hints:   -> wi 4   \/ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  725  jaoa  728  imorr  729  pm2.53  730  pm1.4  735  imorri  757  ioran  760  pm3.14  761  pm1.2  764  orim12i  767  pm1.5  773  pm2.41  784  pm2.42  785  pm2.4  786  pm4.44  787  pm4.78i  790  jaoian  803  jao1i  804  pm2.64  809  pm2.76  816  pm2.82  820  pm3.2ni  821  andi  826  dcim  849  condcOLD  862  pm2.61ddc  869  pm5.18dc  891  pm2.85dc  913  peircedc  922  dcor  944  pm4.42r  980  oplem1  984  ifp2  989  ifpiddc  1000  1fpid3  1003  xoranor  1422  biassdc  1440  anxordi  1445  19.33  1533  hbequid  1562  hbor  1595  19.30dc  1676  19.43  1677  19.32r  1728  hbae  1766  equvini  1806  equveli  1807  exdistrfor  1848  dveeq2  1863  dveeq2or  1864  sbequi  1887  nfsbxy  1995  nfsbxyt  1996  sbcomxyyz  2025  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  modc  2123  mooran1  2152  moexexdc  2164  rgen2a  2587  r19.32r  2680  eueq2dc  2980  eueq3dc  2981  sbcor  3077  elun  3350  ssun  3388  inss  3439  undif3ss  3470  elif  3621  ifsbdc  3622  ifiddc  3645  eqifdc  3646  ifnotdc  3648  ifandc  3650  ifordc  3651  elpr2  3695  rabsnifsb  3741  sssnr  3841  ssprr  3844  sstpr  3845  preq12b  3858  elpr2elpr  3864  exmidn0m  4297  copsexg  4342  sotritric  4427  regexmidlem1  4637  nn0eln0  4724  xpeq0r  5166  funtpg  5388  acexmidlemcase  6023  acexmidlem2  6025  el2oss1o  6654  nnm00  6741  djuss  7329  eldju2ndl  7331  eldju2ndr  7332  updjud  7341  nnnninf2  7386  sspw1or2  7463  exmidonfinlem  7464  exmidfodomrlemim  7472  exmidaclem  7483  renfdisj  8298  sup3exmid  9196  nn0ge0  9486  elnnnn0b  9505  xnn0xr  9531  xnn0nemnf  9537  elnn0z  9553  nn0n0n1ge2b  9620  nn0le2is012  9623  nn0ind-raph  9658  uzin  9850  elnn1uz2  9902  indstr2  9904  nn0ledivnn  10063  xrnemnf  10073  xrnepnf  10074  mnfltxr  10082  nn0pnfge0  10087  xnn0lenn0nn0  10161  xnn0xadd0  10163  elfzonlteqm1  10518  xqltnle  10590  fldiv4p1lem1div2  10628  fldiv4lem1div2  10630  flqeqceilz  10643  modfzo0difsn  10720  m1expcl2  10886  m1expeven  10911  zzlesq  11033  facp1  11055  faclbnd3  11068  bcn1  11083  hashinfuni  11102  hashfzp1  11151  swrdnd  11306  pfxccatin12  11380  swrdccat  11382  pfxccat3a  11385  isumz  12030  arisum  12139  arisum2  12140  ntrivcvgap  12189  prod1dc  12227  fprodfac  12256  mulsucdiv2z  12526  nn0o1gt2  12546  nno  12547  nn0o  12548  dfgcd2  12665  mulgcd  12667  gcdmultiplez  12672  dvdssq  12682  cncongr2  12756  prm2orodd  12778  dfphi2  12872  nnnn0modprm0  12908  prm23lt5  12916  pcmptcl  12995  oddprmdvds  13007  4sqlem19  13062  mulgnn0gsum  13795  recnprss  15498  dvexp2  15523  dvmptid  15527  coseq0negpitopi  15647  lgslem4  15822  gausslemma2dlem0i  15876  lgsquadlem2  15897  2lgslem3  15920  2lgs  15923  2lgsoddprmlem3  15930  upgrm  16041  upgrfi  16043  upgrex  16044  upgruhgr  16052  uspgrushgr  16121  uhgr2edg  16147  usgredg4  16156  upgriswlkdc  16301  umgrclwwlkge2  16343  eupth2lem3lem4fi  16414  konigsberg  16434  bj-dcstab  16474  bj-nn0suc  16680  bj-inf2vnlem2  16687  bj-nn0sucALT  16694  012of  16713  2o01f  16714