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  ianorr  657  pm3.14  658  pm1.2  661  orim12i  664  pm1.5  670  pm2.41  681  pm2.42  682  pm2.4  683  pm4.44  684  jaoian  697  pm2.64  702  pm2.76  709  pm2.82  713  pm3.2ni  714  andi  720  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  868  oplem1  872  xoranor  1250  biassdc  1266  anxordi  1271  19.33  1352  hbequid  1388  hbor  1421  19.30dc  1501  19.43  1502  19.32r  1551  hbae  1587  equvini  1623  equveli  1624  exdistrfor  1663  dveeq2  1678  dveeq2or  1679  sbequi  1702  nfsbxy  1799  nfsbxyt  1800  sbcomxyyz  1827  dvelimALT  1867  dvelimfv  1868  dvelimor  1875  modc  1924  mooran1  1953  moexexdc  1966  rgen2a  2351  r19.32r  2433  eueq2dc  2689  eueq3dc  2690  sbcor  2782  sspssr  3021  elun  3062  ssun  3100  inss  3144  undif3ss  3176  elpr2  3346  sssnr  3476  ssprr  3479  sstpr  3480  preq12b  3493  copsexg  3933  xpeq0r  4640  funtpg  4843  acexmidlemcase  5400  acexmidlem2  5402
  Copyright terms: Public domain W3C validator