Theorem jaoi 711

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

Syntax hints:   → wi 4   ∨ wo 703

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  jaod  712  jaoa  715  imorr  716  pm2.53  717  pm1.4  722  imorri  744  ioran  747  pm3.14  748  pm1.2  751  orim12i  754  pm1.5  760  pm2.41  771  pm2.42  772  pm2.4  773  pm4.44  774  pm4.78i  777  jaoian  790  jao1i  791  pm2.64  796  pm2.76  803  pm2.82  807  pm3.2ni  808  andi  813  dcim  836  condcOLD  849  pm2.61ddc  856  pm5.18dc  878  pm2.85dc  900  peircedc  909  dcan  928  dcor  930  pm4.42r  966  oplem1  970  xoranor  1372  biassdc  1390  anxordi  1395  19.33  1477  hbequid  1506  hbor  1539  19.30dc  1620  19.43  1621  19.32r  1673  hbae  1711  equvini  1751  equveli  1752  exdistrfor  1793  dveeq2  1808  dveeq2or  1809  sbequi  1832  nfsbxy  1935  nfsbxyt  1936  sbcomxyyz  1965  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  modc  2062  mooran1  2091  moexexdc  2103  rgen2a  2524  r19.32r  2616  eueq2dc  2903  eueq3dc  2904  sbcor  2999  elun  3268  ssun  3306  inss  3357  undif3ss  3388  ifsbdc  3538  ifiddc  3559  eqifdc  3560  ifnotdc  3562  ifandc  3563  ifordc  3564  elpr2  3605  sssnr  3740  ssprr  3743  sstpr  3744  preq12b  3757  exmidn0m  4187  copsexg  4229  sotritric  4309  regexmidlem1  4517  nn0eln0  4604  xpeq0r  5033  funtpg  5249  acexmidlemcase  5848  acexmidlem2  5850  el2oss1o  6422  nnm00  6509  djuss  7047  eldju2ndl  7049  eldju2ndr  7050  updjud  7059  nnnninf2  7103  exmidonfinlem  7170  exmidfodomrlemim  7178  exmidaclem  7185  renfdisj  7979  sup3exmid  8873  nn0ge0  9160  elnnnn0b  9179  xnn0xr  9203  xnn0nemnf  9209  elnn0z  9225  nn0n0n1ge2b  9291  nn0le2is012  9294  nn0ind-raph  9329  uzin  9519  elnn1uz2  9566  indstr2  9568  nn0ledivnn  9724  xrnemnf  9734  xrnepnf  9735  mnfltxr  9743  nn0pnfge0  9748  xnn0lenn0nn0  9822  xnn0xadd0  9824  elfzonlteqm1  10166  fldiv4p1lem1div2  10261  flqeqceilz  10274  modfzo0difsn  10351  m1expcl2  10498  m1expeven  10523  facp1  10664  faclbnd3  10677  bcn1  10692  hashinfuni  10711  hashfzp1  10759  isumz  11352  arisum  11461  arisum2  11462  ntrivcvgap  11511  prod1dc  11549  fprodfac  11578  mulsucdiv2z  11844  nn0o1gt2  11864  nno  11865  nn0o  11866  dfgcd2  11969  mulgcd  11971  gcdmultiplez  11976  dvdssq  11986  cncongr2  12058  prm2orodd  12080  dfphi2  12174  nnnn0modprm0  12209  prm23lt5  12217  pcmptcl  12294  oddprmdvds  12306  recnprss  13450  dvexp2  13470  coseq0negpitopi  13551  lgslem4  13698  bj-dcstab  13791  bj-nn0suc  13999  bj-inf2vnlem2  14006  bj-nn0sucALT  14013  012of  14028  2o01f  14029