Theorem jaoi 721

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  722  jaoa  725  imorr  726  pm2.53  727  pm1.4  732  imorri  754  ioran  757  pm3.14  758  pm1.2  761  orim12i  764  pm1.5  770  pm2.41  781  pm2.42  782  pm2.4  783  pm4.44  784  pm4.78i  787  jaoian  800  jao1i  801  pm2.64  806  pm2.76  813  pm2.82  817  pm3.2ni  818  andi  823  dcim  846  condcOLD  859  pm2.61ddc  866  pm5.18dc  888  pm2.85dc  910  peircedc  919  dcor  941  pm4.42r  977  oplem1  981  ifp2  986  ifpiddc  997  1fpid3  1000  xoranor  1419  biassdc  1437  anxordi  1442  19.33  1530  hbequid  1559  hbor  1592  19.30dc  1673  19.43  1674  19.32r  1726  hbae  1764  equvini  1804  equveli  1805  exdistrfor  1846  dveeq2  1861  dveeq2or  1862  sbequi  1885  nfsbxy  1993  nfsbxyt  1994  sbcomxyyz  2023  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  modc  2121  mooran1  2150  moexexdc  2162  rgen2a  2584  r19.32r  2677  eueq2dc  2976  eueq3dc  2977  sbcor  3073  elun  3345  ssun  3383  inss  3434  undif3ss  3465  elif  3614  ifsbdc  3615  ifiddc  3638  eqifdc  3639  ifnotdc  3641  ifandc  3643  ifordc  3644  elpr2  3688  sssnr  3831  ssprr  3834  sstpr  3835  preq12b  3848  elpr2elpr  3854  exmidn0m  4285  copsexg  4330  sotritric  4415  regexmidlem1  4625  nn0eln0  4712  xpeq0r  5151  funtpg  5372  acexmidlemcase  6002  acexmidlem2  6004  el2oss1o  6597  nnm00  6684  djuss  7248  eldju2ndl  7250  eldju2ndr  7251  updjud  7260  nnnninf2  7305  exmidonfinlem  7382  exmidfodomrlemim  7390  exmidaclem  7401  renfdisj  8217  sup3exmid  9115  nn0ge0  9405  elnnnn0b  9424  xnn0xr  9448  xnn0nemnf  9454  elnn0z  9470  nn0n0n1ge2b  9537  nn0le2is012  9540  nn0ind-raph  9575  uzin  9767  elnn1uz2  9814  indstr2  9816  nn0ledivnn  9975  xrnemnf  9985  xrnepnf  9986  mnfltxr  9994  nn0pnfge0  9999  xnn0lenn0nn0  10073  xnn0xadd0  10075  elfzonlteqm1  10428  xqltnle  10499  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  flqeqceilz  10552  modfzo0difsn  10629  m1expcl2  10795  m1expeven  10820  zzlesq  10942  facp1  10964  faclbnd3  10977  bcn1  10992  hashinfuni  11011  hashfzp1  11059  swrdnd  11206  pfxccatin12  11280  swrdccat  11282  pfxccat3a  11285  isumz  11915  arisum  12024  arisum2  12025  ntrivcvgap  12074  prod1dc  12112  fprodfac  12141  mulsucdiv2z  12411  nn0o1gt2  12431  nno  12432  nn0o  12433  dfgcd2  12550  mulgcd  12552  gcdmultiplez  12557  dvdssq  12567  cncongr2  12641  prm2orodd  12663  dfphi2  12757  nnnn0modprm0  12793  prm23lt5  12801  pcmptcl  12880  oddprmdvds  12892  4sqlem19  12947  mulgnn0gsum  13680  recnprss  15376  dvexp2  15401  dvmptid  15405  coseq0negpitopi  15525  lgslem4  15697  gausslemma2dlem0i  15751  lgsquadlem2  15772  2lgslem3  15795  2lgs  15798  2lgsoddprmlem3  15805  upgrm  15915  upgrfi  15917  upgrex  15918  upgruhgr  15926  uspgrushgr  15993  uhgr2edg  16019  usgredg4  16028  upgriswlkdc  16101  umgrclwwlkge2  16139  bj-dcstab  16175  bj-nn0suc  16382  bj-inf2vnlem2  16389  bj-nn0sucALT  16396  012of  16416  2o01f  16417