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  3305  ssun  3343  inss  3394  undif3ss  3425  ifsbdc  3574  ifiddc  3596  eqifdc  3597  ifnotdc  3599  ifandc  3600  ifordc  3601  elpr2  3645  sssnr  3784  ssprr  3787  sstpr  3788  preq12b  3801  exmidn0m  4235  copsexg  4278  sotritric  4360  regexmidlem1  4570  nn0eln0  4657  xpeq0r  5093  funtpg  5310  acexmidlemcase  5920  acexmidlem2  5922  el2oss1o  6510  nnm00  6597  djuss  7145  eldju2ndl  7147  eldju2ndr  7148  updjud  7157  nnnninf2  7202  exmidonfinlem  7272  exmidfodomrlemim  7280  exmidaclem  7291  renfdisj  8103  sup3exmid  9001  nn0ge0  9291  elnnnn0b  9310  xnn0xr  9334  xnn0nemnf  9340  elnn0z  9356  nn0n0n1ge2b  9422  nn0le2is012  9425  nn0ind-raph  9460  uzin  9651  elnn1uz2  9698  indstr2  9700  nn0ledivnn  9859  xrnemnf  9869  xrnepnf  9870  mnfltxr  9878  nn0pnfge0  9883  xnn0lenn0nn0  9957  xnn0xadd0  9959  elfzonlteqm1  10303  xqltnle  10374  fldiv4p1lem1div2  10412  fldiv4lem1div2  10414  flqeqceilz  10427  modfzo0difsn  10504  m1expcl2  10670  m1expeven  10695  zzlesq  10817  facp1  10839  faclbnd3  10852  bcn1  10867  hashinfuni  10886  hashfzp1  10933  isumz  11571  arisum  11680  arisum2  11681  ntrivcvgap  11730  prod1dc  11768  fprodfac  11797  mulsucdiv2z  12067  nn0o1gt2  12087  nno  12088  nn0o  12089  dfgcd2  12206  mulgcd  12208  gcdmultiplez  12213  dvdssq  12223  cncongr2  12297  prm2orodd  12319  dfphi2  12413  nnnn0modprm0  12449  prm23lt5  12457  pcmptcl  12536  oddprmdvds  12548  4sqlem19  12603  mulgnn0gsum  13334  recnprss  15007  dvexp2  15032  dvmptid  15036  coseq0negpitopi  15156  lgslem4  15328  gausslemma2dlem0i  15382  lgsquadlem2  15403  2lgslem3  15426  2lgs  15429  2lgsoddprmlem3  15436  bj-dcstab  15486  bj-nn0suc  15694  bj-inf2vnlem2  15701  bj-nn0sucALT  15708  012of  15724  2o01f  15725