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  1954  nfsbxyt  1955  sbcomxyyz  1984  dvelimALT  2022  dvelimfv  2023  dvelimor  2030  modc  2081  mooran1  2110  moexexdc  2122  rgen2a  2544  r19.32r  2636  eueq2dc  2925  eueq3dc  2926  sbcor  3022  elun  3291  ssun  3329  inss  3380  undif3ss  3411  ifsbdc  3561  ifiddc  3583  eqifdc  3584  ifnotdc  3586  ifandc  3587  ifordc  3588  elpr2  3629  sssnr  3768  ssprr  3771  sstpr  3772  preq12b  3785  exmidn0m  4219  copsexg  4262  sotritric  4342  regexmidlem1  4550  nn0eln0  4637  xpeq0r  5069  funtpg  5286  acexmidlemcase  5892  acexmidlem2  5894  el2oss1o  6469  nnm00  6556  djuss  7100  eldju2ndl  7102  eldju2ndr  7103  updjud  7112  nnnninf2  7156  exmidonfinlem  7223  exmidfodomrlemim  7231  exmidaclem  7238  renfdisj  8048  sup3exmid  8945  nn0ge0  9232  elnnnn0b  9251  xnn0xr  9275  xnn0nemnf  9281  elnn0z  9297  nn0n0n1ge2b  9363  nn0le2is012  9366  nn0ind-raph  9401  uzin  9592  elnn1uz2  9639  indstr2  9641  nn0ledivnn  9799  xrnemnf  9809  xrnepnf  9810  mnfltxr  9818  nn0pnfge0  9823  xnn0lenn0nn0  9897  xnn0xadd0  9899  elfzonlteqm1  10242  xqltnle  10300  fldiv4p1lem1div2  10338  flqeqceilz  10351  modfzo0difsn  10428  m1expcl2  10576  m1expeven  10601  zzlesq  10723  facp1  10745  faclbnd3  10758  bcn1  10773  hashinfuni  10792  hashfzp1  10839  isumz  11432  arisum  11541  arisum2  11542  ntrivcvgap  11591  prod1dc  11629  fprodfac  11658  mulsucdiv2z  11925  nn0o1gt2  11945  nno  11946  nn0o  11947  dfgcd2  12050  mulgcd  12052  gcdmultiplez  12057  dvdssq  12067  cncongr2  12139  prm2orodd  12161  dfphi2  12255  nnnn0modprm0  12290  prm23lt5  12298  pcmptcl  12377  oddprmdvds  12389  4sqlem19  12444  mulgnn0gsum  13085  recnprss  14633  dvexp2  14653  coseq0negpitopi  14734  lgslem4  14882  2lgsoddprmlem3  14937  bj-dcstab  14986  bj-nn0suc  15194  bj-inf2vnlem2  15201  bj-nn0sucALT  15208  012of  15224  2o01f  15225