Theorem jaoi 716

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

Syntax hints:   → wi 4   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  717  jaoa  720  imorr  721  pm2.53  722  pm1.4  727  imorri  749  ioran  752  pm3.14  753  pm1.2  756  orim12i  759  pm1.5  765  pm2.41  776  pm2.42  777  pm2.4  778  pm4.44  779  pm4.78i  782  jaoian  795  jao1i  796  pm2.64  801  pm2.76  808  pm2.82  812  pm3.2ni  813  andi  818  dcim  841  condcOLD  854  pm2.61ddc  861  pm5.18dc  883  pm2.85dc  905  peircedc  914  dcan  933  dcor  935  pm4.42r  971  oplem1  975  xoranor  1377  biassdc  1395  anxordi  1400  19.33  1482  hbequid  1511  hbor  1544  19.30dc  1625  19.43  1626  19.32r  1678  hbae  1716  equvini  1756  equveli  1757  exdistrfor  1798  dveeq2  1813  dveeq2or  1814  sbequi  1837  nfsbxy  1940  nfsbxyt  1941  sbcomxyyz  1970  dvelimALT  2008  dvelimfv  2009  dvelimor  2016  modc  2067  mooran1  2096  moexexdc  2108  rgen2a  2529  r19.32r  2621  eueq2dc  2908  eueq3dc  2909  sbcor  3005  elun  3274  ssun  3312  inss  3363  undif3ss  3394  ifsbdc  3544  ifiddc  3565  eqifdc  3566  ifnotdc  3568  ifandc  3569  ifordc  3570  elpr2  3611  sssnr  3749  ssprr  3752  sstpr  3753  preq12b  3766  exmidn0m  4196  copsexg  4238  sotritric  4318  regexmidlem1  4526  nn0eln0  4613  xpeq0r  5043  funtpg  5259  acexmidlemcase  5860  acexmidlem2  5862  el2oss1o  6434  nnm00  6521  djuss  7059  eldju2ndl  7061  eldju2ndr  7062  updjud  7071  nnnninf2  7115  exmidonfinlem  7182  exmidfodomrlemim  7190  exmidaclem  7197  renfdisj  7991  sup3exmid  8887  nn0ge0  9174  elnnnn0b  9193  xnn0xr  9217  xnn0nemnf  9223  elnn0z  9239  nn0n0n1ge2b  9305  nn0le2is012  9308  nn0ind-raph  9343  uzin  9533  elnn1uz2  9580  indstr2  9582  nn0ledivnn  9738  xrnemnf  9748  xrnepnf  9749  mnfltxr  9757  nn0pnfge0  9762  xnn0lenn0nn0  9836  xnn0xadd0  9838  elfzonlteqm1  10180  fldiv4p1lem1div2  10275  flqeqceilz  10288  modfzo0difsn  10365  m1expcl2  10512  m1expeven  10537  facp1  10678  faclbnd3  10691  bcn1  10706  hashinfuni  10725  hashfzp1  10772  isumz  11365  arisum  11474  arisum2  11475  ntrivcvgap  11524  prod1dc  11562  fprodfac  11591  mulsucdiv2z  11857  nn0o1gt2  11877  nno  11878  nn0o  11879  dfgcd2  11982  mulgcd  11984  gcdmultiplez  11989  dvdssq  11999  cncongr2  12071  prm2orodd  12093  dfphi2  12187  nnnn0modprm0  12222  prm23lt5  12230  pcmptcl  12307  oddprmdvds  12319  recnprss  13736  dvexp2  13756  coseq0negpitopi  13837  lgslem4  13984  bj-dcstab  14077  bj-nn0suc  14285  bj-inf2vnlem2  14292  bj-nn0sucALT  14299  012of  14314  2o01f  14315