Theorem jaoi 728

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  jaod  729  jaoa  732  imorr  733  pm2.53  734  pm1.4  739  imorri  761  ioran  764  pm3.14  765  pm1.2  768  orim12i  771  pm1.5  777  pm2.41  788  pm2.42  789  pm2.4  790  pm4.44  791  pm4.78i  794  jaoian  807  jao1i  808  pm2.64  813  pm2.76  820  pm2.82  824  pm3.2ni  825  andi  830  dcim  853  condcOLD  866  pm2.61ddc  873  pm5.18dc  895  pm2.85dc  917  peircedc  926  dcor  948  pm4.42r  984  oplem1  988  ifp2  993  ifpiddc  1004  1fpid3  1007  xoranor  1426  biassdc  1444  anxordi  1449  19.33  1537  hbequid  1566  hbor  1599  19.30dc  1680  19.43  1681  19.32r  1732  hbae  1770  equvini  1811  equveli  1812  exdistrfor  1853  dveeq2  1868  dveeq2or  1869  sbequi  1892  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  modc  2130  mooran1  2159  moexexdc  2171  rgen2a  2604  r19.32r  2697  eueq2dc  2999  eueq3dc  3000  sbcor  3096  elun  3370  ssun  3408  inss  3461  undif3ss  3492  elif  3652  ifsbdc  3653  ifiddc  3676  eqifdc  3677  ifnotdc  3679  ifandc  3681  ifordc  3682  elpr2  3731  rabsnifsb  3777  sssnr  3878  ssprr  3881  sstpr  3882  preq12b  3895  elpr2elpr  3901  exmidn0m  4340  copsexg  4386  sotritric  4471  regexmidlem1  4682  nn0eln0  4769  xpeq0r  5213  funtpg  5435  acexmidlemcase  6083  acexmidlem2  6085  el2oss1o  6721  nnm00  6808  djuss  7416  eldju2ndl  7418  eldju2ndr  7419  updjud  7428  nnnninf2  7473  sspw1or2  7550  exmidonfinlem  7551  exmidfodomrlemim  7559  exmidaclem  7570  renfdisj  8391  sup3exmid  9295  nn0ge0  9599  elnnnn0b  9618  xnn0xr  9644  xnn0nemnf  9650  elnn0z  9666  nn0n0n1ge2b  9734  nn0le2is012  9737  nn0ind-raph  9773  uzin  9970  elnn1uz2  10022  indstr2  10024  nn0ledivnn  10184  xrnemnf  10195  xrnepnf  10196  mnfltxr  10204  nn0pnfge0  10209  xnn0lenn0nn0  10283  xnn0xadd0  10285  elfzonlteqm1  10644  xqltnle  10718  flapcl  10727  flaplelt  10729  flapge  10736  fldiv4p1lem1div2  10760  fldiv4lem1div2  10762  flqeqceilz  10775  modfzo0difsn  10852  m1expcl2  11018  m1expeven  11043  resq01  11115  zzlesq  11166  facp1  11189  faclbnd3  11202  bcn1  11217  hashinfuni  11237  hashfzp1  11286  swrdnd  11452  pfxccatin12  11526  swrdccat  11528  pfxccat3a  11531  sq01  11681  isumz  12180  arisum  12289  arisum2  12290  ntrivcvgap  12339  prod1dc  12377  fprodfac  12406  mulsucdiv2z  12676  nn0o1gt2  12696  nno  12697  nn0o  12698  dfgcd2  12815  mulgcd  12817  gcdmultiplez  12822  dvdssq  12832  cncongr2  12906  prm2orodd  12928  dfphi2  13026  nnnn0modprm0  13062  prm23lt5  13070  pcmptcl  13149  oddprmdvds  13161  4sqlem19  13216  mulgnn0gzsum  13989  recnprss  15930  dvexp2  15955  dvmptid  15959  coseq0negpitopi  16080  logfac  16143  lgslem4  16344  gausslemma2dlem0i  16398  lgsquadlem2  16419  2lgslem3  16442  2lgs  16445  2lgsoddprmlem3  16452  upgrm  16563  upgrfi  16565  upgrex  16566  upgruhgr  16574  uspgrushgr  16643  uhgr2edg  16669  usgredg4  16678  upgriswlkdc  16823  umgrclwwlkge2  16865  eupth2lem3lem4fi  16936  konigsberg  16956  bj-dcstab  17006  bj-nn0suc  17212  bj-inf2vnlem2  17219  bj-nn0sucALT  17226  012of  17245  2o01f  17246  idjudju  17269