Theorem jaoi 723

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	⊢ (𝜑 → 𝜓)
jaoi.2	⊢ (𝜒 → 𝜓)

Assertion

Ref	Expression
jaoi	⊢ ((𝜑 ∨ 𝜒) → 𝜓)

Proof of Theorem jaoi

Step	Hyp	Ref	Expression
1		jaoi.1	. 2 ⊢ (𝜑 → 𝜓)
2		jaoi.2	. 2 ⊢ (𝜒 → 𝜓)
3		pm3.44 722	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)) → ((𝜑 ∨ 𝜒) → 𝜓))
4	1, 2, 3	mp2an 426	1 ⊢ ((𝜑 ∨ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∨ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  724  jaoa  727  imorr  728  pm2.53  729  pm1.4  734  imorri  756  ioran  759  pm3.14  760  pm1.2  763  orim12i  766  pm1.5  772  pm2.41  783  pm2.42  784  pm2.4  785  pm4.44  786  pm4.78i  789  jaoian  802  jao1i  803  pm2.64  808  pm2.76  815  pm2.82  819  pm3.2ni  820  andi  825  dcim  848  condcOLD  861  pm2.61ddc  868  pm5.18dc  890  pm2.85dc  912  peircedc  921  dcor  943  pm4.42r  979  oplem1  983  ifp2  988  ifpiddc  999  1fpid3  1002  xoranor  1421  biassdc  1439  anxordi  1444  19.33  1532  hbequid  1561  hbor  1594  19.30dc  1675  19.43  1676  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  2586  r19.32r  2679  eueq2dc  2979  eueq3dc  2980  sbcor  3076  elun  3348  ssun  3386  inss  3437  undif3ss  3468  elif  3617  ifsbdc  3618  ifiddc  3641  eqifdc  3642  ifnotdc  3644  ifandc  3646  ifordc  3647  elpr2  3691  rabsnifsb  3737  sssnr  3836  ssprr  3839  sstpr  3840  preq12b  3853  elpr2elpr  3859  exmidn0m  4291  copsexg  4336  sotritric  4421  regexmidlem1  4631  nn0eln0  4718  xpeq0r  5159  funtpg  5381  acexmidlemcase  6013  acexmidlem2  6015  el2oss1o  6611  nnm00  6698  djuss  7269  eldju2ndl  7271  eldju2ndr  7272  updjud  7281  nnnninf2  7326  sspw1or2  7403  exmidonfinlem  7404  exmidfodomrlemim  7412  exmidaclem  7423  renfdisj  8239  sup3exmid  9137  nn0ge0  9427  elnnnn0b  9446  xnn0xr  9470  xnn0nemnf  9476  elnn0z  9492  nn0n0n1ge2b  9559  nn0le2is012  9562  nn0ind-raph  9597  uzin  9789  elnn1uz2  9841  indstr2  9843  nn0ledivnn  10002  xrnemnf  10012  xrnepnf  10013  mnfltxr  10021  nn0pnfge0  10026  xnn0lenn0nn0  10100  xnn0xadd0  10102  elfzonlteqm1  10456  xqltnle  10528  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  flqeqceilz  10581  modfzo0difsn  10658  m1expcl2  10824  m1expeven  10849  zzlesq  10971  facp1  10993  faclbnd3  11006  bcn1  11021  hashinfuni  11040  hashfzp1  11089  swrdnd  11244  pfxccatin12  11318  swrdccat  11320  pfxccat3a  11323  isumz  11968  arisum  12077  arisum2  12078  ntrivcvgap  12127  prod1dc  12165  fprodfac  12194  mulsucdiv2z  12464  nn0o1gt2  12484  nno  12485  nn0o  12486  dfgcd2  12603  mulgcd  12605  gcdmultiplez  12610  dvdssq  12620  cncongr2  12694  prm2orodd  12716  dfphi2  12810  nnnn0modprm0  12846  prm23lt5  12854  pcmptcl  12933  oddprmdvds  12945  4sqlem19  13000  mulgnn0gsum  13733  recnprss  15430  dvexp2  15455  dvmptid  15459  coseq0negpitopi  15579  lgslem4  15751  gausslemma2dlem0i  15805  lgsquadlem2  15826  2lgslem3  15849  2lgs  15852  2lgsoddprmlem3  15859  upgrm  15970  upgrfi  15972  upgrex  15973  upgruhgr  15981  uspgrushgr  16050  uhgr2edg  16076  usgredg4  16085  upgriswlkdc  16230  umgrclwwlkge2  16272  eupth2lem3lem4fi  16343  konigsberg  16363  bj-dcstab  16403  bj-nn0suc  16610  bj-inf2vnlem2  16617  bj-nn0sucALT  16624  012of  16643  2o01f  16644