Theorem jaoi 705

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

Syntax hints:   → wi 4   ∨ wo 697

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 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  jaod  706  jaoa  709  imorr  710  pm2.53  711  pm1.4  716  imorri  738  ioran  741  pm3.14  742  pm1.2  745  orim12i  748  pm1.5  754  pm2.41  765  pm2.42  766  pm2.4  767  pm4.44  768  pm4.78i  771  jaoian  784  jao1i  785  pm2.64  790  pm2.76  797  pm2.82  801  pm3.2ni  802  andi  807  dcim  826  condcOLD  839  pm2.61ddc  846  pm5.18dc  868  pm2.85dc  890  peircedc  899  dcan  918  dcor  919  pm4.42r  955  oplem1  959  xoranor  1355  biassdc  1373  anxordi  1378  19.33  1460  hbequid  1493  hbor  1525  19.30dc  1606  19.43  1607  19.32r  1658  hbae  1696  equvini  1731  equveli  1732  exdistrfor  1772  dveeq2  1787  dveeq2or  1788  sbequi  1811  nfsbxy  1913  nfsbxyt  1914  sbcomxyyz  1943  dvelimALT  1983  dvelimfv  1984  dvelimor  1991  modc  2040  mooran1  2069  moexexdc  2081  rgen2a  2484  r19.32r  2576  eueq2dc  2852  eueq3dc  2853  sbcor  2948  elun  3212  ssun  3250  inss  3301  undif3ss  3332  ifsbdc  3481  ifiddc  3500  eqifdc  3501  ifandc  3503  elpr2  3544  sssnr  3675  ssprr  3678  sstpr  3679  preq12b  3692  exmidn0m  4119  copsexg  4161  sotritric  4241  regexmidlem1  4443  nn0eln0  4528  xpeq0r  4956  funtpg  5169  acexmidlemcase  5762  acexmidlem2  5764  nnm00  6418  djuss  6948  eldju2ndl  6950  eldju2ndr  6951  updjud  6960  exmidonfinlem  7042  exmidfodomrlemim  7050  exmidaclem  7057  renfdisj  7817  sup3exmid  8708  nn0ge0  8995  elnnnn0b  9014  xnn0xr  9038  xnn0nemnf  9044  elnn0z  9060  nn0n0n1ge2b  9123  nn0le2is012  9126  nn0ind-raph  9161  uzin  9351  elnn1uz2  9394  indstr2  9396  nn0ledivnn  9547  xrnemnf  9557  xrnepnf  9558  mnfltxr  9565  nn0pnfge0  9570  xnn0lenn0nn0  9641  xnn0xadd0  9643  elfzonlteqm1  9980  fldiv4p1lem1div2  10071  flqeqceilz  10084  modfzo0difsn  10161  m1expcl2  10308  m1expeven  10333  facp1  10469  faclbnd3  10482  bcn1  10497  hashinfuni  10516  hashfzp1  10563  isumz  11151  arisum  11260  arisum2  11261  ntrivcvgap  11310  mulsucdiv2z  11571  nn0o1gt2  11591  nno  11592  nn0o  11593  dfgcd2  11691  mulgcd  11693  gcdmultiplez  11698  dvdssq  11708  cncongr2  11774  prm2orodd  11796  dfphi2  11885  recnprss  12814  dvexp2  12834  coseq0negpitopi  12906  bj-dcstab  12950  bj-nn0suc  13151  bj-inf2vnlem2  13158  bj-nn0sucALT  13165  el2oss1o  13177  isomninnlem  13214