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  1396  biassdc  1414  anxordi  1419  19.33  1506  hbequid  1535  hbor  1568  19.30dc  1649  19.43  1650  19.32r  1702  hbae  1740  equvini  1780  equveli  1781  exdistrfor  1822  dveeq2  1837  dveeq2or  1838  sbequi  1861  nfsbxy  1969  nfsbxyt  1970  sbcomxyyz  1999  dvelimALT  2037  dvelimfv  2038  dvelimor  2045  modc  2096  mooran1  2125  moexexdc  2137  rgen2a  2559  r19.32r  2651  eueq2dc  2945  eueq3dc  2946  sbcor  3042  elun  3313  ssun  3351  inss  3402  undif3ss  3433  ifsbdc  3582  ifiddc  3605  eqifdc  3606  ifnotdc  3608  ifandc  3609  ifordc  3610  elpr2  3654  sssnr  3793  ssprr  3796  sstpr  3797  preq12b  3810  exmidn0m  4244  copsexg  4287  sotritric  4370  regexmidlem1  4580  nn0eln0  4667  xpeq0r  5104  funtpg  5324  acexmidlemcase  5938  acexmidlem2  5940  el2oss1o  6528  nnm00  6615  djuss  7171  eldju2ndl  7173  eldju2ndr  7174  updjud  7183  nnnninf2  7228  exmidonfinlem  7300  exmidfodomrlemim  7308  exmidaclem  7319  renfdisj  8131  sup3exmid  9029  nn0ge0  9319  elnnnn0b  9338  xnn0xr  9362  xnn0nemnf  9368  elnn0z  9384  nn0n0n1ge2b  9451  nn0le2is012  9454  nn0ind-raph  9489  uzin  9680  elnn1uz2  9727  indstr2  9729  nn0ledivnn  9888  xrnemnf  9898  xrnepnf  9899  mnfltxr  9907  nn0pnfge0  9912  xnn0lenn0nn0  9986  xnn0xadd0  9988  elfzonlteqm1  10337  xqltnle  10408  fldiv4p1lem1div2  10446  fldiv4lem1div2  10448  flqeqceilz  10461  modfzo0difsn  10538  m1expcl2  10704  m1expeven  10729  zzlesq  10851  facp1  10873  faclbnd3  10886  bcn1  10901  hashinfuni  10920  hashfzp1  10967  isumz  11642  arisum  11751  arisum2  11752  ntrivcvgap  11801  prod1dc  11839  fprodfac  11868  mulsucdiv2z  12138  nn0o1gt2  12158  nno  12159  nn0o  12160  dfgcd2  12277  mulgcd  12279  gcdmultiplez  12284  dvdssq  12294  cncongr2  12368  prm2orodd  12390  dfphi2  12484  nnnn0modprm0  12520  prm23lt5  12528  pcmptcl  12607  oddprmdvds  12619  4sqlem19  12674  mulgnn0gsum  13406  recnprss  15101  dvexp2  15126  dvmptid  15130  coseq0negpitopi  15250  lgslem4  15422  gausslemma2dlem0i  15476  lgsquadlem2  15497  2lgslem3  15520  2lgs  15523  2lgsoddprmlem3  15530  bj-dcstab  15625  bj-nn0suc  15833  bj-inf2vnlem2  15840  bj-nn0sucALT  15847  012of  15863  2o01f  15864