ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jaoi GIF version

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
StepHypRef Expression
1 jaoi.1 . 2 (𝜑𝜓)
2 jaoi.2 . 2 (𝜒𝜓)
3 pm3.44 705 . 2 (((𝜑𝜓) ∧ (𝜒𝜓)) → ((𝜑𝜒) → 𝜓))
41, 2, 3mp2an 423 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff set class
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  827  condcOLD  840  pm2.61ddc  847  pm5.18dc  869  pm2.85dc  891  peircedc  900  dcan  919  dcor  920  pm4.42r  956  oplem1  960  xoranor  1356  biassdc  1374  anxordi  1379  19.33  1461  hbequid  1494  hbor  1526  19.30dc  1607  19.43  1608  19.32r  1659  hbae  1697  equvini  1732  equveli  1733  exdistrfor  1773  dveeq2  1788  dveeq2or  1789  sbequi  1812  nfsbxy  1916  nfsbxyt  1917  sbcomxyyz  1946  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  modc  2043  mooran1  2072  moexexdc  2084  rgen2a  2489  r19.32r  2581  eueq2dc  2860  eueq3dc  2861  sbcor  2956  elun  3221  ssun  3259  inss  3310  undif3ss  3341  ifsbdc  3490  ifiddc  3509  eqifdc  3510  ifandc  3512  elpr2  3553  sssnr  3687  ssprr  3690  sstpr  3691  preq12b  3704  exmidn0m  4131  copsexg  4173  sotritric  4253  regexmidlem1  4455  nn0eln0  4540  xpeq0r  4968  funtpg  5181  acexmidlemcase  5776  acexmidlem2  5778  nnm00  6432  djuss  6962  eldju2ndl  6964  eldju2ndr  6965  updjud  6974  exmidonfinlem  7065  exmidfodomrlemim  7073  exmidaclem  7080  renfdisj  7847  sup3exmid  8738  nn0ge0  9025  elnnnn0b  9044  xnn0xr  9068  xnn0nemnf  9074  elnn0z  9090  nn0n0n1ge2b  9153  nn0le2is012  9156  nn0ind-raph  9191  uzin  9381  elnn1uz2  9427  indstr2  9429  nn0ledivnn  9583  xrnemnf  9593  xrnepnf  9594  mnfltxr  9601  nn0pnfge0  9606  xnn0lenn0nn0  9677  xnn0xadd0  9679  elfzonlteqm1  10017  fldiv4p1lem1div2  10108  flqeqceilz  10121  modfzo0difsn  10198  m1expcl2  10345  m1expeven  10370  facp1  10507  faclbnd3  10520  bcn1  10535  hashinfuni  10554  hashfzp1  10601  isumz  11189  arisum  11298  arisum2  11299  ntrivcvgap  11348  mulsucdiv2z  11616  nn0o1gt2  11636  nno  11637  nn0o  11638  dfgcd2  11736  mulgcd  11738  gcdmultiplez  11743  dvdssq  11753  cncongr2  11819  prm2orodd  11841  dfphi2  11930  recnprss  12862  dvexp2  12882  coseq0negpitopi  12963  bj-dcstab  13130  bj-nn0suc  13331  bj-inf2vnlem2  13338  bj-nn0sucALT  13345  el2oss1o  13357  012of  13361  2o01f  13362
  Copyright terms: Public domain W3C validator