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

Theorem impcom 123
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 122 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem is referenced by:  mpan9  275  19.41h  1616  19.41  1617  equtr2  1639  mopick  2021  2euex  2030  gencl  2640  2gencl  2641  rspccva  2709  indifdir  3236  sseq0  3301  minel  3321  r19.2m  3345  elelpwi  3411  ssuni  3643  trintssm  3911  ssexg  3937  pofun  4095  sowlin  4103  2optocl  4463  3optocl  4464  elrnmpt1  4633  resieq  4670  fnun  5056  fss  5105  fun  5114  dmfex  5130  fvelimab  5282  mptfvex  5309  fmptco  5383  fnressn  5402  fressnfv  5403  fvtp2g  5423  fvtp3g  5424  fnex  5436  funfvima3  5445  isores3  5507  f1o2ndf1  5901  reldmtpos  5923  smores  5962  tfrlem7  5987  tfrlemi1  6002  tfrexlem  6004  tfrcl  6034  frecrdg  6078  nnacl  6145  nnmcl  6146  nnmsucr  6153  nntri3or  6158  nnaword  6172  nnaordex  6188  2ecoptocl  6282  ssct  6384  enm  6386  xpf1o  6407  ac6sfi  6455  f1dmvrnfibi  6485  f1vrnfibi  6486  updjud  6576  elni2  6636  ax1rid  7175  negf1o  7623  mulgt1  8078  lbreu  8160  nnaddcl  8196  nnmulcl  8197  zaddcllempos  8539  zaddcllemneg  8541  nn0n0n1ge2b  8578  fzind  8613  fnn0ind  8614  uzaddcl  8825  uzsubsubfz  9212  elfz1b  9253  elfz0ubfz0  9283  fz0fzdiffz0  9288  elfzmlbp  9290  fzofzim  9344  elfzom1elp1fzo  9358  elfzom1p1elfzo  9370  ssfzo12bi  9381  modfzo0difsn  9547  iseqvalt  9602  iseqoveq  9610  iseqss  9611  iseqsst  9612  expivallem  9644  expcllem  9654  expap0  9673  faclbnd  9835  faclbnd6  9838  fihashf1rn  9883  omgadd  9896  hashfzp1  9918  cjexp  9999  r19.29uz  10097  resqrexlemover  10115  resqrexlemlo  10118  resqrexlemcalc3  10121  absexp  10184  fimaxre2  10328  climshft  10362  climub  10401  climserile  10402  dvdsdivcl  10476  dvdsfac  10486  oddnn02np1  10505  oddge22np1  10506  evennn02n  10507  evennn2n  10508  m1exp1  10526  nn0o  10532  flodddiv4  10559  gcdneg  10598  bezoutlemmain  10612  dfgcd2  10628  gcdmultiple  10634  ialginv  10654  cncongr1  10710  prmdvdsexp  10752  prmndvdsfaclt  10760  bdssexg  10980  bj-findis  11059
  Copyright terms: Public domain W3C validator