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  1354  hbequid  1388  hbor  1421  19.30dc  1502  19.43  1503  19.32r  1553  hbae  1589  equvini  1624  equveli  1625  exdistrfor  1664  dveeq2  1679  dveeq2or  1680  sbequi  1703  nfsbxy  1801  nfsbxyt  1802  sbcomxyyz  1829  dvelimALT  1869  dvelimfv  1870  dvelimor  1877  modc  1926  mooran1  1955  moexexdc  1967  rgen2a  2352  r19.32r  2434  eueq2dc  2690  eueq3dc  2691  sbcor  2783  sspssr  3019  elun  3060  ssun  3098  inss  3142  undif3ss  3174  elpr2  3368  sssnr  3497  ssprr  3500  sstpr  3501  preq12b  3514  copsexg  3954  sotritric  4034  regexmidlem1  4200  nn0eln0  4266  xpeq0r  4671  funtpg  4874  acexmidlemcase  5429  acexmidlem2  5431  nnm00  6008
  Copyright terms: Public domain W3C validator