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  4338  copsexg  4384  sotritric  4469  regexmidlem1  4680  nn0eln0  4767  xpeq0r  5210  funtpg  5432  acexmidlemcase  6080  acexmidlem2  6082  el2oss1o  6716  nnm00  6803  djuss  7410  eldju2ndl  7412  eldju2ndr  7413  updjud  7422  nnnninf2  7467  sspw1or2  7544  exmidonfinlem  7545  exmidfodomrlemim  7553  exmidaclem  7564  renfdisj  8385  sup3exmid  9289  nn0ge0  9592  elnnnn0b  9611  xnn0xr  9639  xnn0nemnf  9645  elnn0z  9661  nn0n0n1ge2b  9729  nn0le2is012  9732  nn0ind-raph  9767  uzin  9964  elnn1uz2  10016  indstr2  10018  nn0ledivnn  10178  xrnemnf  10189  xrnepnf  10190  mnfltxr  10198  nn0pnfge0  10203  xnn0lenn0nn0  10277  xnn0xadd0  10279  elfzonlteqm1  10638  xqltnle  10712  flapcl  10721  flaplelt  10723  flapge  10730  fldiv4p1lem1div2  10753  fldiv4lem1div2  10755  flqeqceilz  10768  modfzo0difsn  10845  m1expcl2  11011  m1expeven  11036  resq01  11108  zzlesq  11159  facp1  11182  faclbnd3  11195  bcn1  11210  hashinfuni  11230  hashfzp1  11279  swrdnd  11445  pfxccatin12  11519  swrdccat  11521  pfxccat3a  11524  sq01  11674  isumz  12172  arisum  12281  arisum2  12282  ntrivcvgap  12331  prod1dc  12369  fprodfac  12398  mulsucdiv2z  12668  nn0o1gt2  12688  nno  12689  nn0o  12690  dfgcd2  12807  mulgcd  12809  gcdmultiplez  12814  dvdssq  12824  cncongr2  12898  prm2orodd  12920  dfphi2  13018  nnnn0modprm0  13054  prm23lt5  13062  pcmptcl  13141  oddprmdvds  13153  4sqlem19  13208  mulgnn0gzsum  13980  recnprss  15837  dvexp2  15862  dvmptid  15866  coseq0negpitopi  15987  logfac  16048  lgslem4  16220  gausslemma2dlem0i  16274  lgsquadlem2  16295  2lgslem3  16318  2lgs  16321  2lgsoddprmlem3  16328  upgrm  16439  upgrfi  16441  upgrex  16442  upgruhgr  16450  uspgrushgr  16519  uhgr2edg  16545  usgredg4  16554  upgriswlkdc  16699  umgrclwwlkge2  16741  eupth2lem3lem4fi  16812  konigsberg  16832  bj-dcstab  16882  bj-nn0suc  17088  bj-inf2vnlem2  17095  bj-nn0sucALT  17102  012of  17121  2o01f  17122