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  1553  19.41  1554  equtr2  1575  mopick  1956  2euex  1965  gencl  2559  2gencl  2560  rspccva  2628  sbcimdv  2796  indifdir  3166  sseq0  3231  minel  3256  r19.2m  3282  elelpwi  3341  ssuni  3572  trint0m  3841  ssexg  3866  pofun  4019  sowlin  4027  2optocl  4340  3optocl  4341  elrnmpt1  4508  resieq  4545  fnun  4927  fss  4976  fun  4984  dmfex  5000  fvelimab  5150  mptfvex  5177  fmptco  5251  fnressn  5270  fressnfv  5271  fvtp2g  5291  fvtp3g  5292  fnex  5304  funfvima3  5313  isores3  5376  f1o2ndf1  5768  reldmtpos  5786  smores  5825  tfrlem7  5851  tfrlemi1  5863  tfrexlem  5866  rdgon  5889  frecrdg  5904  nnacl  5970  nnmcl  5971  nnmsucr  5978  nntri3or  5983  nnaword  5991  nnaordex  6007  2ecoptocl  6101  elni2  6168  ax1rid  6570  bdssexg  7319  bj-findis  7393
  Copyright terms: Public domain W3C validator