Theorem jaoi 706

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

Syntax hints:   → wi 4   ∨ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  jaod  707  jaoa  710  imorr  711  pm2.53  712  pm1.4  717  imorri  739  ioran  742  pm3.14  743  pm1.2  746  orim12i  749  pm1.5  755  pm2.41  766  pm2.42  767  pm2.4  768  pm4.44  769  pm4.78i  772  jaoian  785  jao1i  786  pm2.64  791  pm2.76  798  pm2.82  802  pm3.2ni  803  andi  808  dcim  831  condcOLD  844  pm2.61ddc  851  pm5.18dc  873  pm2.85dc  895  peircedc  904  dcan  923  dcor  925  pm4.42r  961  oplem1  965  xoranor  1367  biassdc  1385  anxordi  1390  19.33  1472  hbequid  1501  hbor  1534  19.30dc  1615  19.43  1616  19.32r  1668  hbae  1706  equvini  1746  equveli  1747  exdistrfor  1788  dveeq2  1803  dveeq2or  1804  sbequi  1827  nfsbxy  1930  nfsbxyt  1931  sbcomxyyz  1960  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  modc  2057  mooran1  2086  moexexdc  2098  rgen2a  2520  r19.32r  2612  eueq2dc  2899  eueq3dc  2900  sbcor  2995  elun  3263  ssun  3301  inss  3352  undif3ss  3383  ifsbdc  3532  ifiddc  3553  eqifdc  3554  ifnotdc  3556  ifandc  3557  elpr2  3598  sssnr  3733  ssprr  3736  sstpr  3737  preq12b  3750  exmidn0m  4180  copsexg  4222  sotritric  4302  regexmidlem1  4510  nn0eln0  4597  xpeq0r  5026  funtpg  5239  acexmidlemcase  5837  acexmidlem2  5839  el2oss1o  6411  nnm00  6497  djuss  7035  eldju2ndl  7037  eldju2ndr  7038  updjud  7047  nnnninf2  7091  exmidonfinlem  7149  exmidfodomrlemim  7157  exmidaclem  7164  renfdisj  7958  sup3exmid  8852  nn0ge0  9139  elnnnn0b  9158  xnn0xr  9182  xnn0nemnf  9188  elnn0z  9204  nn0n0n1ge2b  9270  nn0le2is012  9273  nn0ind-raph  9308  uzin  9498  elnn1uz2  9545  indstr2  9547  nn0ledivnn  9703  xrnemnf  9713  xrnepnf  9714  mnfltxr  9722  nn0pnfge0  9727  xnn0lenn0nn0  9801  xnn0xadd0  9803  elfzonlteqm1  10145  fldiv4p1lem1div2  10240  flqeqceilz  10253  modfzo0difsn  10330  m1expcl2  10477  m1expeven  10502  facp1  10643  faclbnd3  10656  bcn1  10671  hashinfuni  10690  hashfzp1  10737  isumz  11330  arisum  11439  arisum2  11440  ntrivcvgap  11489  prod1dc  11527  fprodfac  11556  mulsucdiv2z  11822  nn0o1gt2  11842  nno  11843  nn0o  11844  dfgcd2  11947  mulgcd  11949  gcdmultiplez  11954  dvdssq  11964  cncongr2  12036  prm2orodd  12058  dfphi2  12152  nnnn0modprm0  12187  prm23lt5  12195  pcmptcl  12272  oddprmdvds  12284  recnprss  13296  dvexp2  13316  coseq0negpitopi  13397  lgslem4  13544  bj-dcstab  13637  bj-nn0suc  13846  bj-inf2vnlem2  13853  bj-nn0sucALT  13860  012of  13875  2o01f  13876