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  1807  equveli  1808  exdistrfor  1849  dveeq2  1864  dveeq2or  1865  sbequi  1888  nfsbxy  1998  nfsbxyt  1999  sbcomxyyz  2028  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  modc  2126  mooran1  2155  moexexdc  2167  rgen2a  2598  r19.32r  2691  eueq2dc  2993  eueq3dc  2994  sbcor  3090  elun  3364  ssun  3402  inss  3455  undif3ss  3486  elif  3638  ifsbdc  3639  ifiddc  3662  eqifdc  3663  ifnotdc  3665  ifandc  3667  ifordc  3668  elpr2  3716  rabsnifsb  3762  sssnr  3862  ssprr  3865  sstpr  3866  preq12b  3879  elpr2elpr  3885  exmidn0m  4319  copsexg  4365  sotritric  4450  regexmidlem1  4660  nn0eln0  4747  xpeq0r  5190  funtpg  5412  acexmidlemcase  6053  acexmidlem2  6055  el2oss1o  6689  nnm00  6776  djuss  7374  eldju2ndl  7376  eldju2ndr  7377  updjud  7386  nnnninf2  7431  sspw1or2  7508  exmidonfinlem  7509  exmidfodomrlemim  7517  exmidaclem  7528  renfdisj  8349  sup3exmid  9248  nn0ge0  9538  elnnnn0b  9557  xnn0xr  9585  xnn0nemnf  9591  elnn0z  9607  nn0n0n1ge2b  9675  nn0le2is012  9678  nn0ind-raph  9713  uzin  9905  elnn1uz2  9957  indstr2  9959  nn0ledivnn  10118  xrnemnf  10129  xrnepnf  10130  mnfltxr  10138  nn0pnfge0  10143  xnn0lenn0nn0  10217  xnn0xadd0  10219  elfzonlteqm1  10577  xqltnle  10651  fldiv4p1lem1div2  10689  fldiv4lem1div2  10691  flqeqceilz  10704  modfzo0difsn  10781  m1expcl2  10947  m1expeven  10972  resq01  11044  zzlesq  11095  facp1  11117  faclbnd3  11130  bcn1  11145  hashinfuni  11165  hashfzp1  11214  swrdnd  11376  pfxccatin12  11450  swrdccat  11452  pfxccat3a  11455  isumz  12100  arisum  12209  arisum2  12210  ntrivcvgap  12259  prod1dc  12297  fprodfac  12326  mulsucdiv2z  12596  nn0o1gt2  12616  nno  12617  nn0o  12618  dfgcd2  12735  mulgcd  12737  gcdmultiplez  12742  dvdssq  12752  cncongr2  12826  prm2orodd  12848  dfphi2  12942  nnnn0modprm0  12978  prm23lt5  12986  pcmptcl  13065  oddprmdvds  13077  4sqlem19  13132  mulgnn0gsum  13881  recnprss  15678  dvexp2  15703  dvmptid  15707  coseq0negpitopi  15827  lgslem4  16002  gausslemma2dlem0i  16056  lgsquadlem2  16077  2lgslem3  16100  2lgs  16103  2lgsoddprmlem3  16110  upgrm  16221  upgrfi  16223  upgrex  16224  upgruhgr  16232  uspgrushgr  16301  uhgr2edg  16327  usgredg4  16336  upgriswlkdc  16481  umgrclwwlkge2  16523  eupth2lem3lem4fi  16594  konigsberg  16614  bj-dcstab  16654  bj-nn0suc  16860  bj-inf2vnlem2  16867  bj-nn0sucALT  16874  012of  16893  2o01f  16894