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  2976  eueq3dc  2977  sbcor  3073  elun  3345  ssun  3383  inss  3434  undif3ss  3465  elif  3614  ifsbdc  3615  ifiddc  3638  eqifdc  3639  ifnotdc  3641  ifandc  3643  ifordc  3644  elpr2  3688  sssnr  3830  ssprr  3833  sstpr  3834  preq12b  3847  elpr2elpr  3853  exmidn0m  4284  copsexg  4329  sotritric  4414  regexmidlem1  4624  nn0eln0  4711  xpeq0r  5150  funtpg  5371  acexmidlemcase  5995  acexmidlem2  5997  el2oss1o  6587  nnm00  6674  djuss  7233  eldju2ndl  7235  eldju2ndr  7236  updjud  7245  nnnninf2  7290  exmidonfinlem  7367  exmidfodomrlemim  7375  exmidaclem  7386  renfdisj  8202  sup3exmid  9100  nn0ge0  9390  elnnnn0b  9409  xnn0xr  9433  xnn0nemnf  9439  elnn0z  9455  nn0n0n1ge2b  9522  nn0le2is012  9525  nn0ind-raph  9560  uzin  9751  elnn1uz2  9798  indstr2  9800  nn0ledivnn  9959  xrnemnf  9969  xrnepnf  9970  mnfltxr  9978  nn0pnfge0  9983  xnn0lenn0nn0  10057  xnn0xadd0  10059  elfzonlteqm1  10411  xqltnle  10482  fldiv4p1lem1div2  10520  fldiv4lem1div2  10522  flqeqceilz  10535  modfzo0difsn  10612  m1expcl2  10778  m1expeven  10803  zzlesq  10925  facp1  10947  faclbnd3  10960  bcn1  10975  hashinfuni  10994  hashfzp1  11041  swrdnd  11186  pfxccatin12  11260  swrdccat  11262  pfxccat3a  11265  isumz  11895  arisum  12004  arisum2  12005  ntrivcvgap  12054  prod1dc  12092  fprodfac  12121  mulsucdiv2z  12391  nn0o1gt2  12411  nno  12412  nn0o  12413  dfgcd2  12530  mulgcd  12532  gcdmultiplez  12537  dvdssq  12547  cncongr2  12621  prm2orodd  12643  dfphi2  12737  nnnn0modprm0  12773  prm23lt5  12781  pcmptcl  12860  oddprmdvds  12872  4sqlem19  12927  mulgnn0gsum  13660  recnprss  15355  dvexp2  15380  dvmptid  15384  coseq0negpitopi  15504  lgslem4  15676  gausslemma2dlem0i  15730  lgsquadlem2  15751  2lgslem3  15774  2lgs  15777  2lgsoddprmlem3  15784  upgrm  15894  upgrfi  15896  upgrex  15897  upgruhgr  15905  uspgrushgr  15972  uhgr2edg  15998  usgredg4  16007  bj-dcstab  16078  bj-nn0suc  16285  bj-inf2vnlem2  16292  bj-nn0sucALT  16299  012of  16316  2o01f  16317