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

Theorem impcom 116
Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
imp.1 (φ → (ψχ))
Assertion
Ref Expression
impcom ((ψ φ) → χ)

Proof of Theorem impcom
StepHypRef Expression
1 imp.1 . . 3 (φ → (ψχ))
21com12 27 . 2 (ψ → (φχ))
32imp 115 1 ((ψ φ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem is referenced by:  mpan9  265  19.41h  1572  19.41  1573  equtr2  1594  mopick  1975  2euex  1984  gencl  2580  2gencl  2581  rspccva  2649  sbcimdv  2817  indifdir  3187  sseq0  3252  minel  3277  r19.2m  3303  elelpwi  3362  ssuni  3593  trint0m  3862  ssexg  3887  pofun  4040  sowlin  4048  2optocl  4360  3optocl  4361  elrnmpt1  4528  resieq  4565  fnun  4948  fss  4997  fun  5006  dmfex  5022  fvelimab  5172  mptfvex  5199  fmptco  5273  fnressn  5292  fressnfv  5293  fvtp2g  5313  fvtp3g  5314  fnex  5326  funfvima3  5335  isores3  5398  f1o2ndf1  5791  reldmtpos  5809  smores  5848  tfrlem7  5874  tfrlemi1  5887  tfrexlem  5889  rdgon  5913  frecrdg  5931  nnacl  5998  nnmcl  5999  nnmsucr  6006  nntri3or  6011  nnaword  6020  nnaordex  6036  2ecoptocl  6130  enm  6230  elni2  6298  ax1rid  6741  mulgt1  7590  nnaddcl  7695  nnmulcl  7696  zaddcllempos  8038  zaddcllemneg  8040  nn0n0n1ge2b  8076  fzind  8109  fnn0ind  8110  uzaddcl  8285  uzsubsubfz  8661  elfz1b  8702  elfz0ubfz0  8732  fz0fzdiffz0  8737  elfzmlbmOLD  8739  elfzmlbp  8740  fzofzim  8794  elfzom1elp1fzo  8808  elfzom1p1elfzo  8820  ssfzo12bi  8831  expivallem  8890  expcllem  8900  expap0  8919  cjexp  9101  bdssexg  9335  bj-findis  9409
  Copyright terms: Public domain W3C validator