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  7411  eldju2ndl  7413  eldju2ndr  7414  updjud  7423  nnnninf2  7468  sspw1or2  7545  exmidonfinlem  7546  exmidfodomrlemim  7554  exmidaclem  7565  renfdisj  8386  sup3exmid  9290  nn0ge0  9593  elnnnn0b  9612  xnn0xr  9640  xnn0nemnf  9646  elnn0z  9662  nn0n0n1ge2b  9730  nn0le2is012  9733  nn0ind-raph  9768  uzin  9965  elnn1uz2  10017  indstr2  10019  nn0ledivnn  10179  xrnemnf  10190  xrnepnf  10191  mnfltxr  10199  nn0pnfge0  10204  xnn0lenn0nn0  10278  xnn0xadd0  10280  elfzonlteqm1  10639  xqltnle  10713  flapcl  10722  flaplelt  10724  flapge  10731  fldiv4p1lem1div2  10755  fldiv4lem1div2  10757  flqeqceilz  10770  modfzo0difsn  10847  m1expcl2  11013  m1expeven  11038  resq01  11110  zzlesq  11161  facp1  11184  faclbnd3  11197  bcn1  11212  hashinfuni  11232  hashfzp1  11281  swrdnd  11447  pfxccatin12  11521  swrdccat  11523  pfxccat3a  11526  sq01  11676  isumz  12175  arisum  12284  arisum2  12285  ntrivcvgap  12334  prod1dc  12372  fprodfac  12401  mulsucdiv2z  12671  nn0o1gt2  12691  nno  12692  nn0o  12693  dfgcd2  12810  mulgcd  12812  gcdmultiplez  12817  dvdssq  12827  cncongr2  12901  prm2orodd  12923  dfphi2  13021  nnnn0modprm0  13057  prm23lt5  13065  pcmptcl  13144  oddprmdvds  13156  4sqlem19  13211  mulgnn0gzsum  13984  recnprss  15879  dvexp2  15904  dvmptid  15908  coseq0negpitopi  16029  logfac  16090  lgslem4  16288  gausslemma2dlem0i  16342  lgsquadlem2  16363  2lgslem3  16386  2lgs  16389  2lgsoddprmlem3  16396  upgrm  16507  upgrfi  16509  upgrex  16510  upgruhgr  16518  uspgrushgr  16587  uhgr2edg  16613  usgredg4  16622  upgriswlkdc  16767  umgrclwwlkge2  16809  eupth2lem3lem4fi  16880  konigsberg  16900  bj-dcstab  16950  bj-nn0suc  17156  bj-inf2vnlem2  17163  bj-nn0sucALT  17170  012of  17189  2o01f  17190