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

Theorem jaoi 620
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 619 . 2 (((φψ) (χψ)) → ((φ χ) → ψ))
41, 2, 3mp2an 402 1 ((φ χ) → ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wo 613
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 614
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  jaod  621  jaoa  624  pm2.53  625  pm1.4  630  imorri  652  ioran  653  pm3.14  654  pm1.2  657  orim12i  660  pm1.5  666  pm2.41  677  pm2.42  678  pm2.4  679  pm4.44  680  jaoian  693  pm2.64  698  pm2.76  705  pm2.82  709  pm3.2ni  710  andi  715  condc  733  pm2.61ddc  742  pm5.18dc  761  dcim  768  imorr  781  pm4.78i  792  pm2.85dc  795  peircedc  804  dcan  824  dcor  825  pm4.42r  860  oplem1  864  xoranor  1248  biassdc  1264  anxordi  1269  19.33  1346  hbequid  1379  hbor  1411  19.30dc  1491  19.43  1492  19.32r  1543  hbae  1579  equvini  1614  equveli  1615  exdistrfor  1654  dveeq2  1669  dveeq2or  1670  sbequi  1693  nfsbxy  1791  nfsbxyt  1792  sbcomxyyz  1819  dvelimALT  1859  dvelimfv  1860  dvelimor  1867  modc  1916  mooran1  1945  moexexdc  1957  rgen2a  2344  r19.32r  2426  eueq2dc  2682  eueq3dc  2683  sbcor  2775  sspssr  3011  elun  3052  ssun  3090  inss  3134  undif3ss  3166  elpr2  3358  sssnr  3487  ssprr  3490  sstpr  3491  preq12b  3504  copsexg  3944  sotritric  4024  regexmidlem1  4190  nn0eln0  4256  xpeq0r  4661  funtpg  4864  acexmidlemcase  5419  acexmidlem2  5421  nnm00  6001  renfdisj  6679  nn0ge0  7781  elnnnn0b  7800  elnn0z  7832  nn0ind-raph  7919  bj-nn0suc  8344  bj-inf2vnlem2  8351  bj-nn0sucALT  8358
  Copyright terms: Public domain W3C validator