Theorem jaoi 669

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

Syntax hints:   → wi 4   ∨ wo 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  jaod  670  jaoa  673  pm2.53  674  pm1.4  679  imorri  701  ioran  702  pm3.14  703  pm1.2  706  orim12i  709  pm1.5  715  pm2.41  726  pm2.42  727  pm2.4  728  pm4.44  729  jaoian  742  jao1i  743  pm2.64  748  pm2.76  755  pm2.82  759  pm3.2ni  760  andi  765  condc  785  pm2.61ddc  794  pm5.18dc  813  dcim  820  imorr  833  pm4.78i  844  pm2.85dc  847  peircedc  856  dcan  878  dcor  879  pm4.42r  915  oplem1  919  xoranor  1311  biassdc  1329  anxordi  1334  19.33  1416  hbequid  1449  hbor  1481  19.30dc  1561  19.43  1562  19.32r  1613  hbae  1650  equvini  1685  equveli  1686  exdistrfor  1725  dveeq2  1740  dveeq2or  1741  sbequi  1764  nfsbxy  1863  nfsbxyt  1864  sbcomxyyz  1891  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  modc  1988  mooran1  2017  moexexdc  2029  rgen2a  2425  r19.32r  2509  eueq2dc  2778  eueq3dc  2779  sbcor  2871  elun  3127  ssun  3165  inss  3215  undif3ss  3246  ifsbdc  3388  eqifdc  3407  elpr2  3447  sssnr  3574  ssprr  3577  sstpr  3578  preq12b  3591  copsexg  4038  sotritric  4118  regexmidlem1  4315  nn0eln0  4399  xpeq0r  4811  funtpg  5021  acexmidlemcase  5589  acexmidlem2  5591  nnm00  6221  djuss  6682  eldju2ndl  6684  eldju2ndr  6685  updjud  6694  exmidfodomrlemim  6748  renfdisj  7467  nn0ge0  8608  elnnnn0b  8627  xnn0xr  8651  xnn0nemnf  8657  elnn0z  8673  nn0n0n1ge2b  8736  nn0ind-raph  8773  uzin  8960  elnn1uz2  9003  indstr2  9005  nn0ledivnn  9147  xrnemnf  9157  xrnepnf  9158  mnfltxr  9165  nn0pnfge0  9170  elfzonlteqm1  9524  fldiv4p1lem1div2  9615  flqeqceilz  9628  modfzo0difsn  9705  m1expcl2  9828  m1expeven  9853  facp1  9987  faclbnd3  10000  bcn1  10015  hashinfuni  10034  hashfzp1  10081  mulsucdiv2z  10679  nn0o1gt2  10699  nno  10700  nn0o  10701  dfgcd2  10797  mulgcd  10799  gcdmultiplez  10804  dvdssq  10814  cncongr2  10880  prm2orodd  10902  dfphi2  10990  bj-nn0suc  11216  bj-inf2vnlem2  11223  bj-nn0sucALT  11230  el2oss1o  11244