Theorem jaoi 706

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

Syntax hints:   → wi 4   ∨ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  jaod  707  jaoa  710  imorr  711  pm2.53  712  pm1.4  717  imorri  739  ioran  742  pm3.14  743  pm1.2  746  orim12i  749  pm1.5  755  pm2.41  766  pm2.42  767  pm2.4  768  pm4.44  769  pm4.78i  772  jaoian  785  jao1i  786  pm2.64  791  pm2.76  798  pm2.82  802  pm3.2ni  803  andi  808  dcim  831  condcOLD  844  pm2.61ddc  851  pm5.18dc  873  pm2.85dc  895  peircedc  904  dcan  923  dcor  924  pm4.42r  960  oplem1  964  xoranor  1366  biassdc  1384  anxordi  1389  19.33  1471  hbequid  1500  hbor  1533  19.30dc  1614  19.43  1615  19.32r  1667  hbae  1705  equvini  1745  equveli  1746  exdistrfor  1787  dveeq2  1802  dveeq2or  1803  sbequi  1826  nfsbxy  1929  nfsbxyt  1930  sbcomxyyz  1959  dvelimALT  1997  dvelimfv  1998  dvelimor  2005  modc  2056  mooran1  2085  moexexdc  2097  rgen2a  2518  r19.32r  2610  eueq2dc  2894  eueq3dc  2895  sbcor  2990  elun  3258  ssun  3296  inss  3347  undif3ss  3378  ifsbdc  3527  ifiddc  3548  eqifdc  3549  ifandc  3551  elpr2  3592  sssnr  3727  ssprr  3730  sstpr  3731  preq12b  3744  exmidn0m  4174  copsexg  4216  sotritric  4296  regexmidlem1  4504  nn0eln0  4591  xpeq0r  5020  funtpg  5233  acexmidlemcase  5831  acexmidlem2  5833  el2oss1o  6402  nnm00  6488  djuss  7026  eldju2ndl  7028  eldju2ndr  7029  updjud  7038  nnnninf2  7082  exmidonfinlem  7140  exmidfodomrlemim  7148  exmidaclem  7155  renfdisj  7949  sup3exmid  8843  nn0ge0  9130  elnnnn0b  9149  xnn0xr  9173  xnn0nemnf  9179  elnn0z  9195  nn0n0n1ge2b  9261  nn0le2is012  9264  nn0ind-raph  9299  uzin  9489  elnn1uz2  9536  indstr2  9538  nn0ledivnn  9694  xrnemnf  9704  xrnepnf  9705  mnfltxr  9713  nn0pnfge0  9718  xnn0lenn0nn0  9792  xnn0xadd0  9794  elfzonlteqm1  10135  fldiv4p1lem1div2  10230  flqeqceilz  10243  modfzo0difsn  10320  m1expcl2  10467  m1expeven  10492  facp1  10632  faclbnd3  10645  bcn1  10660  hashinfuni  10679  hashfzp1  10726  isumz  11316  arisum  11425  arisum2  11426  ntrivcvgap  11475  prod1dc  11513  fprodfac  11542  mulsucdiv2z  11807  nn0o1gt2  11827  nno  11828  nn0o  11829  dfgcd2  11932  mulgcd  11934  gcdmultiplez  11939  dvdssq  11949  cncongr2  12015  prm2orodd  12037  dfphi2  12129  nnnn0modprm0  12164  prm23lt5  12172  pcmptcl  12249  oddprmdvds  12261  recnprss  13197  dvexp2  13217  coseq0negpitopi  13298  bj-dcstab  13470  bj-nn0suc  13681  bj-inf2vnlem2  13688  bj-nn0sucALT  13695  012of  13709  2o01f  13710