Theorem jaoi 636

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

Syntax hints:   → wi 4   ∨ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  jaod  637  jaoa  640  pm2.53  641  pm1.4  646  imorri  668  ioran  669  pm3.14  670  pm1.2  673  orim12i  676  pm1.5  682  pm2.41  693  pm2.42  694  pm2.4  695  pm4.44  696  jaoian  709  pm2.64  714  pm2.76  721  pm2.82  725  pm3.2ni  726  andi  731  condc  749  pm2.61ddc  758  pm5.18dc  777  dcim  784  imorr  797  pm4.78i  808  pm2.85dc  811  peircedc  820  dcan  842  dcor  843  pm4.42r  878  oplem1  882  xoranor  1268  biassdc  1286  anxordi  1291  19.33  1373  hbequid  1406  hbor  1438  19.30dc  1518  19.43  1519  19.32r  1570  hbae  1606  equvini  1641  equveli  1642  exdistrfor  1681  dveeq2  1696  dveeq2or  1697  sbequi  1720  nfsbxy  1818  nfsbxyt  1819  sbcomxyyz  1846  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  modc  1943  mooran1  1972  moexexdc  1984  rgen2a  2375  r19.32r  2457  eueq2dc  2714  eueq3dc  2715  sbcor  2807  sspssr  3043  elun  3084  ssun  3122  inss  3166  undif3ss  3198  elpr2  3397  sssnr  3524  ssprr  3527  sstpr  3528  preq12b  3541  copsexg  3981  sotritric  4061  regexmidlem1  4258  nn0eln0  4341  xpeq0r  4746  funtpg  4950  acexmidlemcase  5507  acexmidlem2  5509  nnm00  6102  renfdisj  7079  nn0ge0  8207  elnnnn0b  8226  elnn0z  8258  nn0n0n1ge2b  8320  nn0ind-raph  8355  uzin  8505  elnn1uz2  8544  indstr2  8546  xrnemnf  8699  xrnepnf  8700  mnfltxr  8707  nn0pnfge0  8712  elfzonlteqm1  9066  fldiv4p1lem1div2  9147  flqeqceilz  9160  m1expcl2  9277  bj-nn0suc  10089  bj-inf2vnlem2  10096  bj-nn0sucALT  10103