ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  impcom 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  1575  19.41  1576  equtr2  1597  mopick  1978  2euex  1987  gencl  2586  2gencl  2587  rspccva  2655  sbcimdv  2823  indifdir  3193  sseq0  3258  minel  3283  r19.2m  3309  elelpwi  3370  ssuni  3602  trint0m  3871  ssexg  3896  pofun  4049  sowlin  4057  2optocl  4417  3optocl  4418  elrnmpt1  4585  resieq  4622  fnun  5005  fss  5054  fun  5063  dmfex  5079  fvelimab  5229  mptfvex  5256  fmptco  5330  fnressn  5349  fressnfv  5350  fvtp2g  5370  fvtp3g  5371  fnex  5383  funfvima3  5392  isores3  5455  f1o2ndf1  5849  reldmtpos  5868  smores  5907  tfrlem7  5933  tfrlemi1  5946  tfrexlem  5948  rdgon  5973  frecrdg  5992  nnacl  6059  nnmcl  6060  nnmsucr  6067  nntri3or  6072  nnaword  6084  nnaordex  6100  2ecoptocl  6194  enm  6294  ac6sfi  6352  elni2  6410  ax1rid  6949  mulgt1  7827  nnaddcl  7932  nnmulcl  7933  zaddcllempos  8280  zaddcllemneg  8282  nn0n0n1ge2b  8318  fzind  8351  fnn0ind  8352  uzaddcl  8527  uzsubsubfz  8909  elfz1b  8950  elfz0ubfz0  8980  fz0fzdiffz0  8985  elfzmlbmOLD  8987  elfzmlbp  8988  fzofzim  9042  elfzom1elp1fzo  9056  elfzom1p1elfzo  9068  ssfzo12bi  9079  iseqss  9200  expivallem  9230  expcllem  9240  expap0  9259  cjexp  9467  r19.29uz  9564  resqrexlemover  9582  resqrexlemlo  9585  resqrexlemcalc3  9588  absexp  9649  climshft  9799  climub  9838  climserile  9839  ialginv  9860  bdssexg  9998  bj-findis  10078
  Copyright terms: Public domain W3C validator