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  1498  hbequid  1527  hbor  1560  19.30dc  1641  19.43  1642  19.32r  1694  hbae  1732  equvini  1772  equveli  1773  exdistrfor  1814  dveeq2  1829  dveeq2or  1830  sbequi  1853  nfsbxy  1961  nfsbxyt  1962  sbcomxyyz  1991  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  modc  2088  mooran1  2117  moexexdc  2129  rgen2a  2551  r19.32r  2643  eueq2dc  2937  eueq3dc  2938  sbcor  3034  elun  3304  ssun  3342  inss  3393  undif3ss  3424  ifsbdc  3573  ifiddc  3595  eqifdc  3596  ifnotdc  3598  ifandc  3599  ifordc  3600  elpr2  3644  sssnr  3783  ssprr  3786  sstpr  3787  preq12b  3800  exmidn0m  4234  copsexg  4277  sotritric  4359  regexmidlem1  4569  nn0eln0  4656  xpeq0r  5092  funtpg  5309  acexmidlemcase  5917  acexmidlem2  5919  el2oss1o  6501  nnm00  6588  djuss  7136  eldju2ndl  7138  eldju2ndr  7139  updjud  7148  nnnninf2  7193  exmidonfinlem  7260  exmidfodomrlemim  7268  exmidaclem  7275  renfdisj  8086  sup3exmid  8984  nn0ge0  9274  elnnnn0b  9293  xnn0xr  9317  xnn0nemnf  9323  elnn0z  9339  nn0n0n1ge2b  9405  nn0le2is012  9408  nn0ind-raph  9443  uzin  9634  elnn1uz2  9681  indstr2  9683  nn0ledivnn  9842  xrnemnf  9852  xrnepnf  9853  mnfltxr  9861  nn0pnfge0  9866  xnn0lenn0nn0  9940  xnn0xadd0  9942  elfzonlteqm1  10286  xqltnle  10357  fldiv4p1lem1div2  10395  fldiv4lem1div2  10397  flqeqceilz  10410  modfzo0difsn  10487  m1expcl2  10653  m1expeven  10678  zzlesq  10800  facp1  10822  faclbnd3  10835  bcn1  10850  hashinfuni  10869  hashfzp1  10916  isumz  11554  arisum  11663  arisum2  11664  ntrivcvgap  11713  prod1dc  11751  fprodfac  11780  mulsucdiv2z  12050  nn0o1gt2  12070  nno  12071  nn0o  12072  dfgcd2  12181  mulgcd  12183  gcdmultiplez  12188  dvdssq  12198  cncongr2  12272  prm2orodd  12294  dfphi2  12388  nnnn0modprm0  12424  prm23lt5  12432  pcmptcl  12511  oddprmdvds  12523  4sqlem19  12578  mulgnn0gsum  13258  recnprss  14923  dvexp2  14948  dvmptid  14952  coseq0negpitopi  15072  lgslem4  15244  gausslemma2dlem0i  15298  lgsquadlem2  15319  2lgslem3  15342  2lgs  15345  2lgsoddprmlem3  15352  bj-dcstab  15402  bj-nn0suc  15610  bj-inf2vnlem2  15617  bj-nn0sucALT  15624  012of  15640  2o01f  15641