Theorem jaoi 717

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

Syntax hints:   → wi 4   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  718  jaoa  721  imorr  722  pm2.53  723  pm1.4  728  imorri  750  ioran  753  pm3.14  754  pm1.2  757  orim12i  760  pm1.5  766  pm2.41  777  pm2.42  778  pm2.4  779  pm4.44  780  pm4.78i  783  jaoian  796  jao1i  797  pm2.64  802  pm2.76  809  pm2.82  813  pm3.2ni  814  andi  819  dcim  842  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.85dc  906  peircedc  915  dcor  937  pm4.42r  973  oplem1  977  xoranor  1388  biassdc  1406  anxordi  1411  19.33  1495  hbequid  1524  hbor  1557  19.30dc  1638  19.43  1639  19.32r  1691  hbae  1729  equvini  1769  equveli  1770  exdistrfor  1811  dveeq2  1826  dveeq2or  1827  sbequi  1850  nfsbxy  1958  nfsbxyt  1959  sbcomxyyz  1988  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  modc  2085  mooran1  2114  moexexdc  2126  rgen2a  2548  r19.32r  2640  eueq2dc  2933  eueq3dc  2934  sbcor  3030  elun  3300  ssun  3338  inss  3389  undif3ss  3420  ifsbdc  3569  ifiddc  3591  eqifdc  3592  ifnotdc  3594  ifandc  3595  ifordc  3596  elpr2  3640  sssnr  3779  ssprr  3782  sstpr  3783  preq12b  3796  exmidn0m  4230  copsexg  4273  sotritric  4355  regexmidlem1  4565  nn0eln0  4652  xpeq0r  5088  funtpg  5305  acexmidlemcase  5913  acexmidlem2  5915  el2oss1o  6496  nnm00  6583  djuss  7129  eldju2ndl  7131  eldju2ndr  7132  updjud  7141  nnnninf2  7186  exmidonfinlem  7253  exmidfodomrlemim  7261  exmidaclem  7268  renfdisj  8079  sup3exmid  8976  nn0ge0  9265  elnnnn0b  9284  xnn0xr  9308  xnn0nemnf  9314  elnn0z  9330  nn0n0n1ge2b  9396  nn0le2is012  9399  nn0ind-raph  9434  uzin  9625  elnn1uz2  9672  indstr2  9674  nn0ledivnn  9833  xrnemnf  9843  xrnepnf  9844  mnfltxr  9852  nn0pnfge0  9857  xnn0lenn0nn0  9931  xnn0xadd0  9933  elfzonlteqm1  10277  xqltnle  10336  fldiv4p1lem1div2  10374  fldiv4lem1div2  10376  flqeqceilz  10389  modfzo0difsn  10466  m1expcl2  10632  m1expeven  10657  zzlesq  10779  facp1  10801  faclbnd3  10814  bcn1  10829  hashinfuni  10848  hashfzp1  10895  isumz  11532  arisum  11641  arisum2  11642  ntrivcvgap  11691  prod1dc  11729  fprodfac  11758  mulsucdiv2z  12026  nn0o1gt2  12046  nno  12047  nn0o  12048  dfgcd2  12151  mulgcd  12153  gcdmultiplez  12158  dvdssq  12168  cncongr2  12242  prm2orodd  12264  dfphi2  12358  nnnn0modprm0  12393  prm23lt5  12401  pcmptcl  12480  oddprmdvds  12492  4sqlem19  12547  mulgnn0gsum  13198  recnprss  14841  dvexp2  14861  coseq0negpitopi  14971  lgslem4  15119  gausslemma2dlem0i  15173  2lgsoddprmlem3  15199  bj-dcstab  15248  bj-nn0suc  15456  bj-inf2vnlem2  15463  bj-nn0sucALT  15470  012of  15486  2o01f  15487