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  6720  nnm00  6807  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  9646  xnn0nemnf  9652  elnn0z  9668  nn0n0n1ge2b  9736  nn0le2is012  9739  nn0ind-raph  9774  uzin  9971  elnn1uz2  10023  indstr2  10025  nn0ledivnn  10185  xrnemnf  10196  xrnepnf  10197  mnfltxr  10205  nn0pnfge0  10210  xnn0lenn0nn0  10284  xnn0xadd0  10286  elfzonlteqm1  10645  xqltnle  10719  flapcl  10728  flaplelt  10730  flapge  10737  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  flqeqceilz  10776  modfzo0difsn  10853  m1expcl2  11019  m1expeven  11044  resq01  11116  zzlesq  11167  facp1  11190  faclbnd3  11203  bcn1  11218  hashinfuni  11238  hashfzp1  11287  swrdnd  11453  pfxccatin12  11527  swrdccat  11529  pfxccat3a  11532  sq01  11682  isumz  12181  arisum  12290  arisum2  12291  ntrivcvgap  12340  prod1dc  12378  fprodfac  12407  mulsucdiv2z  12677  nn0o1gt2  12697  nno  12698  nn0o  12699  dfgcd2  12816  mulgcd  12818  gcdmultiplez  12823  dvdssq  12833  cncongr2  12907  prm2orodd  12929  dfphi2  13027  nnnn0modprm0  13063  prm23lt5  13071  pcmptcl  13150  oddprmdvds  13162  4sqlem19  13217  mulgnn0gzsum  13990  recnprss  15913  dvexp2  15938  dvmptid  15942  coseq0negpitopi  16063  logfac  16126  lgslem4  16327  gausslemma2dlem0i  16381  lgsquadlem2  16402  2lgslem3  16425  2lgs  16428  2lgsoddprmlem3  16435  upgrm  16546  upgrfi  16548  upgrex  16549  upgruhgr  16557  uspgrushgr  16626  uhgr2edg  16652  usgredg4  16661  upgriswlkdc  16806  umgrclwwlkge2  16848  eupth2lem3lem4fi  16919  konigsberg  16939  bj-dcstab  16989  bj-nn0suc  17195  bj-inf2vnlem2  17202  bj-nn0sucALT  17209  012of  17228  2o01f  17229  idjudju  17252