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	⊢ (𝜑 → 𝜓)
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 720	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)) → ((𝜑 ∨ 𝜒) → 𝜓))
4	1, 2, 3	mp2an 426	1 ⊢ ((𝜑 ∨ 𝜒) → 𝜓)

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  2977  eueq3dc  2978  sbcor  3074  elun  3346  ssun  3384  inss  3435  undif3ss  3466  elif  3615  ifsbdc  3616  ifiddc  3639  eqifdc  3640  ifnotdc  3642  ifandc  3644  ifordc  3645  elpr2  3689  rabsnifsb  3735  sssnr  3834  ssprr  3837  sstpr  3838  preq12b  3851  elpr2elpr  3857  exmidn0m  4289  copsexg  4334  sotritric  4419  regexmidlem1  4629  nn0eln0  4716  xpeq0r  5157  funtpg  5378  acexmidlemcase  6008  acexmidlem2  6010  el2oss1o  6606  nnm00  6693  djuss  7260  eldju2ndl  7262  eldju2ndr  7263  updjud  7272  nnnninf2  7317  exmidonfinlem  7394  exmidfodomrlemim  7402  exmidaclem  7413  renfdisj  8229  sup3exmid  9127  nn0ge0  9417  elnnnn0b  9436  xnn0xr  9460  xnn0nemnf  9466  elnn0z  9482  nn0n0n1ge2b  9549  nn0le2is012  9552  nn0ind-raph  9587  uzin  9779  elnn1uz2  9831  indstr2  9833  nn0ledivnn  9992  xrnemnf  10002  xrnepnf  10003  mnfltxr  10011  nn0pnfge0  10016  xnn0lenn0nn0  10090  xnn0xadd0  10092  elfzonlteqm1  10445  xqltnle  10517  fldiv4p1lem1div2  10555  fldiv4lem1div2  10557  flqeqceilz  10570  modfzo0difsn  10647  m1expcl2  10813  m1expeven  10838  zzlesq  10960  facp1  10982  faclbnd3  10995  bcn1  11010  hashinfuni  11029  hashfzp1  11078  swrdnd  11230  pfxccatin12  11304  swrdccat  11306  pfxccat3a  11309  isumz  11940  arisum  12049  arisum2  12050  ntrivcvgap  12099  prod1dc  12137  fprodfac  12166  mulsucdiv2z  12436  nn0o1gt2  12456  nno  12457  nn0o  12458  dfgcd2  12575  mulgcd  12577  gcdmultiplez  12582  dvdssq  12592  cncongr2  12666  prm2orodd  12688  dfphi2  12782  nnnn0modprm0  12818  prm23lt5  12826  pcmptcl  12905  oddprmdvds  12917  4sqlem19  12972  mulgnn0gsum  13705  recnprss  15401  dvexp2  15426  dvmptid  15430  coseq0negpitopi  15550  lgslem4  15722  gausslemma2dlem0i  15776  lgsquadlem2  15797  2lgslem3  15820  2lgs  15823  2lgsoddprmlem3  15830  upgrm  15941  upgrfi  15943  upgrex  15944  upgruhgr  15952  uspgrushgr  16019  uhgr2edg  16045  usgredg4  16054  upgriswlkdc  16157  umgrclwwlkge2  16197  bj-dcstab  16288  bj-nn0suc  16495  bj-inf2vnlem2  16502  bj-nn0sucALT  16509  012of  16528  2o01f  16529