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  6012  acexmidlem2  6014  el2oss1o  6610  nnm00  6697  djuss  7268  eldju2ndl  7270  eldju2ndr  7271  updjud  7280  nnnninf2  7325  sspw1or2  7402  exmidonfinlem  7403  exmidfodomrlemim  7411  exmidaclem  7422  renfdisj  8238  sup3exmid  9136  nn0ge0  9426  elnnnn0b  9445  xnn0xr  9469  xnn0nemnf  9475  elnn0z  9491  nn0n0n1ge2b  9558  nn0le2is012  9561  nn0ind-raph  9596  uzin  9788  elnn1uz2  9840  indstr2  9842  nn0ledivnn  10001  xrnemnf  10011  xrnepnf  10012  mnfltxr  10020  nn0pnfge0  10025  xnn0lenn0nn0  10099  xnn0xadd0  10101  elfzonlteqm1  10454  xqltnle  10526  fldiv4p1lem1div2  10564  fldiv4lem1div2  10566  flqeqceilz  10579  modfzo0difsn  10656  m1expcl2  10822  m1expeven  10847  zzlesq  10969  facp1  10991  faclbnd3  11004  bcn1  11019  hashinfuni  11038  hashfzp1  11087  swrdnd  11239  pfxccatin12  11313  swrdccat  11315  pfxccat3a  11318  isumz  11949  arisum  12058  arisum2  12059  ntrivcvgap  12108  prod1dc  12146  fprodfac  12175  mulsucdiv2z  12445  nn0o1gt2  12465  nno  12466  nn0o  12467  dfgcd2  12584  mulgcd  12586  gcdmultiplez  12591  dvdssq  12601  cncongr2  12675  prm2orodd  12697  dfphi2  12791  nnnn0modprm0  12827  prm23lt5  12835  pcmptcl  12914  oddprmdvds  12926  4sqlem19  12981  mulgnn0gsum  13714  recnprss  15410  dvexp2  15435  dvmptid  15439  coseq0negpitopi  15559  lgslem4  15731  gausslemma2dlem0i  15785  lgsquadlem2  15806  2lgslem3  15829  2lgs  15832  2lgsoddprmlem3  15839  upgrm  15950  upgrfi  15952  upgrex  15953  upgruhgr  15961  uspgrushgr  16030  uhgr2edg  16056  usgredg4  16065  upgriswlkdc  16210  umgrclwwlkge2  16252  bj-dcstab  16352  bj-nn0suc  16559  bj-inf2vnlem2  16566  bj-nn0sucALT  16573  012of  16592  2o01f  16593