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

Theorem expcom 114
Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
exp.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
expcom (𝜓 → (𝜑𝜒))

Proof of Theorem expcom
StepHypRef Expression
1 exp.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 113 . 2 (𝜑 → (𝜓𝜒))
32com12 30 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-ia3 106
This theorem is referenced by:  ancoms  264  syldan  276  sylan  277  pm4.79dc  843  dedlema  911  dedlemb  912  19.35-1  1556  cbval2  1838  cbvex2  1839  r19.21be  2453  r19.35-1  2505  mosubt  2770  sbcrext  2892  uneqdifeqim  3335  ssuni  3631  uniss2  3640  elpwuni  3770  elssabg  3931  elpw2g  3939  epelg  4053  elnn  4354  relop  4514  riinint  4621  cnviinm  4889  funopg  4964  fun  5094  tz6.12c  5235  fvelrnb  5253  fmptco  5362  fnressn  5381  fressnfv  5382  fvtp2g  5402  fvtp3g  5403  fconst2g  5408  isores3  5486  isoselem  5490  eloprabga  5622  fo1stresm  5819  poxp  5884  brtpos2  5900  smores  5941  tfrlem1  5957  tfrlemi1  5981  tfr1onlemaccex  5997  tfrcllemaccex  6010  frecrdg  6057  oawordriexmid  6114  nnacl  6124  nnmcl  6125  nnacom  6128  nnaass  6129  nnmsucr  6132  nnmordi  6155  iinerm  6244  th3qlem2  6275  brdomg  6295  f1domg  6305  ssdomg  6325  nndomo  6399  carden2bex  6517  addclpi  6579  addnidpig  6588  genpassl  6776  genpassu  6777  nqprloc  6797  ltaprlem  6870  recexprlemopl  6877  recexprlemopu  6879  recexprlemupu  6880  recexprlemss1l  6887  recexprlemss1u  6888  cauappcvgprlemupu  6901  caucvgprlemupu  6924  caucvgprprlemupu  6952  archsr  7020  peano2nnnn  7083  receuap  7826  peano2nn  8118  nnaddcl  8126  zrevaddcl  8482  nzadd  8484  zdiv  8516  nneo  8531  zeo2  8534  peano5uzti  8536  fzind  8543  fnn0ind  8544  lbzbi  8782  qrevaddcl  8810  irradd  8812  irrmul  8813  ltsubrp  8849  ltaddrp  8850  icoshft  9088  fzen  9138  elfzm11  9184  uzsplit  9185  fzoval  9235  elfzom1elp1fzo  9288  exfzdc  9326  modaddmodup  9469  frec2uzrdg  9491  iseqoveq  9540  iseqss  9541  iseqsst  9542  iseqfveq2  9544  iseqshft2  9548  monoord  9551  iseqsplit  9554  iseqcaopr3  9556  iseqid3s  9562  iseqid2  9564  iseqhomo  9565  iseqz  9566  expadd  9615  expmul  9618  leexp1a  9628  faccl  9759  facdiv  9762  faclbnd  9765  faclbnd6  9768  omgadd  9826  sizeunsng  9831  shftlem  9842  resqrexlemover  10034  resqrexlemdecn  10036  resqrexlemlo  10037  resqrexlemcalc3  10040  climub  10320  climserile  10321  dvds2ln  10373  dvdsabseq  10392  dvdsdivcl  10395  alzdvds  10399  oddnn02np1  10424  m1exp1  10445  nn0o1gt2  10449  nno  10450  ndvdsadd  10475  flodddiv4  10478  gcddiv  10552  gcdmultiple  10553  gcdmultiplez  10554  rplpwr  10560  dvdssq  10564  nn0seqcvgd  10567  ialginv  10573  ialgcvga  10577  ialgfx  10578  isprm2  10643  isprm3  10644  prmdvdsexp  10671  2spim  10755
  Copyright terms: Public domain W3C validator