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  9287  nn0ge0  9588  elnnnn0b  9607  xnn0xr  9635  xnn0nemnf  9641  elnn0z  9657  nn0n0n1ge2b  9725  nn0le2is012  9728  nn0ind-raph  9763  uzin  9955  elnn1uz2  10007  indstr2  10009  nn0ledivnn  10168  xrnemnf  10179  xrnepnf  10180  mnfltxr  10188  nn0pnfge0  10193  xnn0lenn0nn0  10267  xnn0xadd0  10269  elfzonlteqm1  10628  xqltnle  10702  fldiv4p1lem1div2  10740  fldiv4lem1div2  10742  flqeqceilz  10755  modfzo0difsn  10832  m1expcl2  10998  m1expeven  11023  resq01  11095  zzlesq  11146  facp1  11168  faclbnd3  11181  bcn1  11196  hashinfuni  11216  hashfzp1  11265  swrdnd  11431  pfxccatin12  11505  swrdccat  11507  pfxccat3a  11510  sq01  11660  isumz  12156  arisum  12265  arisum2  12266  ntrivcvgap  12315  prod1dc  12353  fprodfac  12382  mulsucdiv2z  12652  nn0o1gt2  12672  nno  12673  nn0o  12674  dfgcd2  12791  mulgcd  12793  gcdmultiplez  12798  dvdssq  12808  cncongr2  12882  prm2orodd  12904  dfphi2  12998  nnnn0modprm0  13034  prm23lt5  13042  pcmptcl  13121  oddprmdvds  13133  4sqlem19  13188  mulgnn0gzsum  13931  recnprss  15788  dvexp2  15813  dvmptid  15817  coseq0negpitopi  15937  logfac  15995  lgslem4  16122  gausslemma2dlem0i  16176  lgsquadlem2  16197  2lgslem3  16220  2lgs  16223  2lgsoddprmlem3  16230  upgrm  16341  upgrfi  16343  upgrex  16344  upgruhgr  16352  uspgrushgr  16421  uhgr2edg  16447  usgredg4  16456  upgriswlkdc  16601  umgrclwwlkge2  16643  eupth2lem3lem4fi  16714  konigsberg  16734  bj-dcstab  16784  bj-nn0suc  16990  bj-inf2vnlem2  16997  bj-nn0sucALT  17004  012of  17023  2o01f  17024