Theorem jaoi 724

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

Syntax hints:   → wi 4   ∨ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  jaod  725  jaoa  728  imorr  729  pm2.53  730  pm1.4  735  imorri  757  ioran  760  pm3.14  761  pm1.2  764  orim12i  767  pm1.5  773  pm2.41  784  pm2.42  785  pm2.4  786  pm4.44  787  pm4.78i  790  jaoian  803  jao1i  804  pm2.64  809  pm2.76  816  pm2.82  820  pm3.2ni  821  andi  826  dcim  849  condcOLD  862  pm2.61ddc  869  pm5.18dc  891  pm2.85dc  913  peircedc  922  dcor  944  pm4.42r  980  oplem1  984  ifp2  989  ifpiddc  1000  1fpid3  1003  xoranor  1422  biassdc  1440  anxordi  1445  19.33  1533  hbequid  1562  hbor  1595  19.30dc  1676  19.43  1677  19.32r  1728  hbae  1766  equvini  1807  equveli  1808  exdistrfor  1849  dveeq2  1864  dveeq2or  1865  sbequi  1888  nfsbxy  1998  nfsbxyt  1999  sbcomxyyz  2028  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  modc  2126  mooran1  2155  moexexdc  2167  rgen2a  2598  r19.32r  2691  eueq2dc  2993  eueq3dc  2994  sbcor  3090  elun  3364  ssun  3402  inss  3455  undif3ss  3486  elif  3638  ifsbdc  3639  ifiddc  3662  eqifdc  3663  ifnotdc  3665  ifandc  3667  ifordc  3668  elpr2  3716  rabsnifsb  3762  sssnr  3862  ssprr  3865  sstpr  3866  preq12b  3879  elpr2elpr  3885  exmidn0m  4319  copsexg  4365  sotritric  4450  regexmidlem1  4660  nn0eln0  4747  xpeq0r  5190  funtpg  5412  acexmidlemcase  6053  acexmidlem2  6055  el2oss1o  6689  nnm00  6776  djuss  7374  eldju2ndl  7376  eldju2ndr  7377  updjud  7386  nnnninf2  7431  sspw1or2  7508  exmidonfinlem  7509  exmidfodomrlemim  7517  exmidaclem  7528  renfdisj  8349  sup3exmid  9251  nn0ge0  9541  elnnnn0b  9560  xnn0xr  9588  xnn0nemnf  9594  elnn0z  9610  nn0n0n1ge2b  9678  nn0le2is012  9681  nn0ind-raph  9716  uzin  9908  elnn1uz2  9960  indstr2  9962  nn0ledivnn  10121  xrnemnf  10132  xrnepnf  10133  mnfltxr  10141  nn0pnfge0  10146  xnn0lenn0nn0  10220  xnn0xadd0  10222  elfzonlteqm1  10580  xqltnle  10654  fldiv4p1lem1div2  10692  fldiv4lem1div2  10694  flqeqceilz  10707  modfzo0difsn  10784  m1expcl2  10950  m1expeven  10975  resq01  11047  zzlesq  11098  facp1  11120  faclbnd3  11133  bcn1  11148  hashinfuni  11168  hashfzp1  11217  swrdnd  11379  pfxccatin12  11453  swrdccat  11455  pfxccat3a  11458  sq01  11608  isumz  12104  arisum  12213  arisum2  12214  ntrivcvgap  12263  prod1dc  12301  fprodfac  12330  mulsucdiv2z  12600  nn0o1gt2  12620  nno  12621  nn0o  12622  dfgcd2  12739  mulgcd  12741  gcdmultiplez  12746  dvdssq  12756  cncongr2  12830  prm2orodd  12852  dfphi2  12946  nnnn0modprm0  12982  prm23lt5  12990  pcmptcl  13069  oddprmdvds  13081  4sqlem19  13136  mulgnn0gsum  13885  recnprss  15682  dvexp2  15707  dvmptid  15711  coseq0negpitopi  15831  lgslem4  16006  gausslemma2dlem0i  16060  lgsquadlem2  16081  2lgslem3  16104  2lgs  16107  2lgsoddprmlem3  16114  upgrm  16225  upgrfi  16227  upgrex  16228  upgruhgr  16236  uspgrushgr  16305  uhgr2edg  16331  usgredg4  16340  upgriswlkdc  16485  umgrclwwlkge2  16527  eupth2lem3lem4fi  16598  konigsberg  16618  bj-dcstab  16668  bj-nn0suc  16874  bj-inf2vnlem2  16881  bj-nn0sucALT  16888  012of  16907  2o01f  16908