Theorem jaoi 674

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

Syntax hints:   → wi 4   ∨ wo 667

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  jaod  675  jaoa  678  pm2.53  679  pm1.4  684  imorri  706  ioran  707  pm3.14  708  pm1.2  711  orim12i  714  pm1.5  720  pm2.41  731  pm2.42  732  pm2.4  733  pm4.44  734  jaoian  747  jao1i  748  pm2.64  753  pm2.76  760  pm2.82  764  pm3.2ni  765  andi  770  condc  790  pm2.61ddc  799  pm5.18dc  818  dcim  825  imorr  838  pm4.78i  849  pm2.85dc  852  peircedc  861  dcan  883  dcor  884  pm4.42r  920  oplem1  924  xoranor  1320  biassdc  1338  anxordi  1343  19.33  1425  hbequid  1458  hbor  1490  19.30dc  1570  19.43  1571  19.32r  1622  hbae  1660  equvini  1695  equveli  1696  exdistrfor  1735  dveeq2  1750  dveeq2or  1751  sbequi  1774  nfsbxy  1873  nfsbxyt  1874  sbcomxyyz  1901  dvelimALT  1941  dvelimfv  1942  dvelimor  1949  modc  1998  mooran1  2027  moexexdc  2039  rgen2a  2440  r19.32r  2528  eueq2dc  2802  eueq3dc  2803  sbcor  2897  elun  3156  ssun  3194  inss  3245  undif3ss  3276  ifsbdc  3425  ifiddc  3444  eqifdc  3445  ifandc  3447  elpr2  3488  sssnr  3619  ssprr  3622  sstpr  3623  preq12b  3636  exmidn0m  4054  copsexg  4095  sotritric  4175  regexmidlem1  4377  nn0eln0  4461  xpeq0r  4887  funtpg  5099  acexmidlemcase  5685  acexmidlem2  5687  nnm00  6328  djuss  6841  eldju2ndl  6843  eldju2ndr  6844  updjud  6853  exmidfodomrlemim  6924  renfdisj  7643  sup3exmid  8515  nn0ge0  8796  elnnnn0b  8815  xnn0xr  8839  xnn0nemnf  8845  elnn0z  8861  nn0n0n1ge2b  8924  nn0le2is012  8927  nn0ind-raph  8962  uzin  9150  elnn1uz2  9193  indstr2  9195  nn0ledivnn  9337  xrnemnf  9347  xrnepnf  9348  mnfltxr  9355  nn0pnfge0  9360  xnn0lenn0nn0  9431  xnn0xadd0  9433  elfzonlteqm1  9770  fldiv4p1lem1div2  9861  flqeqceilz  9874  modfzo0difsn  9951  m1expcl2  10092  m1expeven  10117  facp1  10253  faclbnd3  10266  bcn1  10281  hashinfuni  10300  hashfzp1  10347  isumz  10932  arisum  11041  arisum2  11042  mulsucdiv2z  11312  nn0o1gt2  11332  nno  11333  nn0o  11334  dfgcd2  11430  mulgcd  11432  gcdmultiplez  11437  dvdssq  11447  cncongr2  11513  prm2orodd  11535  dfphi2  11623  bj-nn0suc  12567  bj-inf2vnlem2  12574  bj-nn0sucALT  12581  el2oss1o  12593