Theorem jaoi 718

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

Syntax hints:   → wi 4   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  719  jaoa  722  imorr  723  pm2.53  724  pm1.4  729  imorri  751  ioran  754  pm3.14  755  pm1.2  758  orim12i  761  pm1.5  767  pm2.41  778  pm2.42  779  pm2.4  780  pm4.44  781  pm4.78i  784  jaoian  797  jao1i  798  pm2.64  803  pm2.76  810  pm2.82  814  pm3.2ni  815  andi  820  dcim  843  condcOLD  856  pm2.61ddc  863  pm5.18dc  885  pm2.85dc  907  peircedc  916  dcor  938  pm4.42r  974  oplem1  978  xoranor  1397  biassdc  1415  anxordi  1420  19.33  1508  hbequid  1537  hbor  1570  19.30dc  1651  19.43  1652  19.32r  1704  hbae  1742  equvini  1782  equveli  1783  exdistrfor  1824  dveeq2  1839  dveeq2or  1840  sbequi  1863  nfsbxy  1971  nfsbxyt  1972  sbcomxyyz  2001  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  modc  2098  mooran1  2127  moexexdc  2139  rgen2a  2561  r19.32r  2653  eueq2dc  2950  eueq3dc  2951  sbcor  3047  elun  3318  ssun  3356  inss  3407  undif3ss  3438  elif  3587  ifsbdc  3588  ifiddc  3611  eqifdc  3612  ifnotdc  3614  ifandc  3615  ifordc  3616  elpr2  3660  sssnr  3800  ssprr  3803  sstpr  3804  preq12b  3817  exmidn0m  4253  copsexg  4296  sotritric  4379  regexmidlem1  4589  nn0eln0  4676  xpeq0r  5114  funtpg  5334  acexmidlemcase  5952  acexmidlem2  5954  el2oss1o  6542  nnm00  6629  djuss  7187  eldju2ndl  7189  eldju2ndr  7190  updjud  7199  nnnninf2  7244  exmidonfinlem  7317  exmidfodomrlemim  7325  exmidaclem  7336  renfdisj  8152  sup3exmid  9050  nn0ge0  9340  elnnnn0b  9359  xnn0xr  9383  xnn0nemnf  9389  elnn0z  9405  nn0n0n1ge2b  9472  nn0le2is012  9475  nn0ind-raph  9510  uzin  9701  elnn1uz2  9748  indstr2  9750  nn0ledivnn  9909  xrnemnf  9919  xrnepnf  9920  mnfltxr  9928  nn0pnfge0  9933  xnn0lenn0nn0  10007  xnn0xadd0  10009  elfzonlteqm1  10361  xqltnle  10432  fldiv4p1lem1div2  10470  fldiv4lem1div2  10472  flqeqceilz  10485  modfzo0difsn  10562  m1expcl2  10728  m1expeven  10753  zzlesq  10875  facp1  10897  faclbnd3  10910  bcn1  10925  hashinfuni  10944  hashfzp1  10991  swrdnd  11135  isumz  11775  arisum  11884  arisum2  11885  ntrivcvgap  11934  prod1dc  11972  fprodfac  12001  mulsucdiv2z  12271  nn0o1gt2  12291  nno  12292  nn0o  12293  dfgcd2  12410  mulgcd  12412  gcdmultiplez  12417  dvdssq  12427  cncongr2  12501  prm2orodd  12523  dfphi2  12617  nnnn0modprm0  12653  prm23lt5  12661  pcmptcl  12740  oddprmdvds  12752  4sqlem19  12807  mulgnn0gsum  13539  recnprss  15234  dvexp2  15259  dvmptid  15263  coseq0negpitopi  15383  lgslem4  15555  gausslemma2dlem0i  15609  lgsquadlem2  15630  2lgslem3  15653  2lgs  15656  2lgsoddprmlem3  15663  upgrm  15771  upgrfi  15773  upgrex  15774  upgruhgr  15782  bj-dcstab  15831  bj-nn0suc  16038  bj-inf2vnlem2  16045  bj-nn0sucALT  16052  012of  16069  2o01f  16070