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

Theorem jaoi 623
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 622 . 2 (((φψ) (χψ)) → ((φ χ) → ψ))
41, 2, 3mp2an 404 1 ((φ χ) → ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wo 616
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  jaod  624  jaoa  627  pm2.53  628  pm1.4  633  imorri  655  ioran  656  pm3.14  657  pm1.2  660  orim12i  663  pm1.5  669  pm2.41  680  pm2.42  681  pm2.4  682  pm4.44  683  jaoian  696  pm2.64  701  pm2.76  708  pm2.82  712  pm3.2ni  713  andi  719  condc  740  pm2.61ddc  751  pm5.18dc  770  dcim  777  imorr  790  pm4.78i  801  pm2.85dc  804  peircedc  813  dcan  830  dcor  831  pm4.42r  866  oplem1  870  xoranor  1253  biassdc  1269  anxordi  1274  19.33  1353  hbequid  1387  hbor  1420  19.30dc  1500  19.43  1501  19.32r  1552  hbae  1588  equvini  1623  equveli  1624  exdistrfor  1663  dveeq2  1678  dveeq2or  1679  sbequi  1702  nfsbxy  1800  nfsbxyt  1801  sbcomxyyz  1828  dvelimALT  1868  dvelimfv  1869  dvelimor  1876  modc  1925  mooran1  1954  moexexdc  1966  rgen2a  2351  r19.32r  2433  eueq2dc  2689  eueq3dc  2690  sbcor  2782  sspssr  3018  elun  3059  ssun  3097  inss  3141  undif3ss  3173  elpr2  3367  sssnr  3496  ssprr  3499  sstpr  3500  preq12b  3513  copsexg  3953  sotritric  4033  regexmidlem1  4200  nn0eln0  4266  xpeq0r  4671  funtpg  4874  acexmidlemcase  5429  acexmidlem2  5431  nnm00  6011  renfdisj  6674  bj-nn0suc  6861  bj-inf2vnlem2  6868  bj-nn0sucALT  6875
  Copyright terms: Public domain W3C validator