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

Theorem impcom 120
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 30 . 2 (𝜓 → (𝜑𝜒))
32imp 119 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem is referenced by:  mpan9  269  19.41h  1591  19.41  1592  equtr2  1613  mopick  1994  2euex  2003  gencl  2603  2gencl  2604  rspccva  2672  indifdir  3220  sseq0  3285  minel  3310  r19.2m  3336  elelpwi  3397  ssuni  3629  trintssm  3897  ssexg  3923  pofun  4076  sowlin  4084  2optocl  4444  3optocl  4445  elrnmpt1  4612  resieq  4649  fnun  5032  fss  5081  fun  5090  dmfex  5106  fvelimab  5256  mptfvex  5283  fmptco  5357  fnressn  5376  fressnfv  5377  fvtp2g  5397  fvtp3g  5398  fnex  5410  funfvima3  5419  isores3  5482  f1o2ndf1  5876  reldmtpos  5898  smores  5937  tfrlem7  5963  tfrlemi1  5976  tfrexlem  5978  rdgon  6003  frecrdg  6022  nnacl  6089  nnmcl  6090  nnmsucr  6097  nntri3or  6102  nnaword  6114  nnaordex  6130  2ecoptocl  6224  enm  6324  ac6sfi  6382  elni2  6469  ax1rid  7008  mulgt1  7903  nnaddcl  8009  nnmulcl  8010  zaddcllempos  8338  zaddcllemneg  8340  nn0n0n1ge2b  8377  fzind  8411  fnn0ind  8412  uzaddcl  8624  uzsubsubfz  9012  elfz1b  9053  elfz0ubfz0  9083  fz0fzdiffz0  9088  elfzmlbmOLD  9090  elfzmlbp  9091  fzofzim  9145  elfzom1elp1fzo  9159  elfzom1p1elfzo  9171  ssfzo12bi  9182  modfzo0difsn  9339  iseqss  9384  expivallem  9415  expcllem  9425  expap0  9444  faclbnd  9602  faclbnd6  9605  cjexp  9714  r19.29uz  9811  resqrexlemover  9829  resqrexlemlo  9832  resqrexlemcalc3  9835  absexp  9898  climshft  10048  climub  10087  climserile  10088  dvdsdivcl  10154  dvdsfac  10164  oddnn02np1  10184  oddge22np1  10185  evennn02n  10186  evennn2n  10187  m1exp1  10205  nn0o  10211  ialginv  10241  bdssexg  10383  bj-findis  10463
  Copyright terms: Public domain W3C validator