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

Theorem expcom 115
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 114 . 2 (𝜑 → (𝜓𝜒))
32com12 30 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  ancoms  266  syldan  278  sylan  279  animpimp2impd  531  pm4.79dc  871  dedlema  936  dedlemb  937  19.35-1  1586  cbval2  1871  cbvex2  1872  nelelne  2375  r19.21be  2498  r19.35-1  2556  mosubt  2832  sbcrext  2956  uneqdifeqim  3416  ssuni  3726  uniss2  3735  elpwuni  3870  elssabg  4041  elpw2g  4049  epelg  4180  elnn  4487  relop  4657  riinint  4768  cnviinm  5048  funopg  5125  fun  5263  tz6.12c  5417  fvelrnb  5435  fmptco  5552  fnressn  5572  fressnfv  5573  fvtp2g  5595  fvtp3g  5596  fconst2g  5601  isores3  5682  isoselem  5687  eloprabga  5824  fo1stresm  6025  poxp  6095  brtpos2  6114  smores  6155  tfrlem1  6171  tfrlemi1  6195  tfr1onlemaccex  6211  tfrcllemaccex  6224  frecrdg  6271  oawordriexmid  6332  nnacl  6342  nnmcl  6343  nnacom  6346  nnaass  6347  nnmsucr  6350  nndifsnid  6369  nnmordi  6378  iinerm  6467  th3qlem2  6498  elpmg  6524  pmss12g  6535  mapsn  6550  brdomg  6608  f1domg  6618  ssdomg  6638  nndomo  6724  elfi2  6826  carden2bex  7011  addclpi  7099  addnidpig  7108  genpassl  7296  genpassu  7297  nqprloc  7317  ltaprlem  7390  recexprlemopl  7397  recexprlemopu  7399  recexprlemupu  7400  recexprlemss1l  7407  recexprlemss1u  7408  cauappcvgprlemupu  7421  caucvgprlemupu  7444  caucvgprprlemupu  7472  archsr  7554  peano2nnnn  7625  receuap  8390  peano2nn  8689  nnaddcl  8697  zrevaddcl  9055  nzadd  9057  zdiv  9090  nneo  9105  zeo2  9108  peano5uzti  9110  fzind  9117  fnn0ind  9118  lbzbi  9357  qrevaddcl  9385  irradd  9387  irrmul  9388  ltsubrp  9424  ltaddrp  9425  xnn0xadd0  9590  icoshft  9713  fzen  9763  elfzm11  9811  uzsplit  9812  fzoval  9865  elfzom1elp1fzo  9919  exfzdc  9957  modaddmodup  10100  frec2uzrdg  10122  seq3clss  10180  monoord  10189  seq3caopr3  10194  seq3f1olemp  10215  seq3id3  10220  seq3homo  10223  seq3z  10224  ser3ge0  10230  expadd  10275  expmul  10278  leexp1a  10288  faccl  10421  facdiv  10424  faclbnd  10427  faclbnd6  10430  omgadd  10488  hashunsng  10493  seq3coll  10525  shftlem  10528  resqrexlemover  10722  resqrexlemdecn  10724  resqrexlemlo  10725  resqrexlemcalc3  10728  climub  11053  climserle  11054  fsumzcl2  11114  fsumsplitsnun  11128  fsum2d  11144  modfsummodlemstep  11166  fsumabs  11174  fsumiun  11186  bcxmas  11198  cvgratnnlemnexp  11233  cvgratnnlemmn  11234  dvds2ln  11422  dvdsabseq  11441  dvdsdivcl  11444  alzdvds  11448  oddnn02np1  11473  m1exp1  11494  nn0o1gt2  11498  nno  11499  ndvdsadd  11524  flodddiv4  11527  gcddiv  11603  gcdmultiple  11604  gcdmultiplez  11605  rplpwr  11611  dvdssq  11615  nn0seqcvgd  11618  alginv  11624  algcvga  11628  algfx  11629  isprm2  11694  isprm3  11695  prmdvdsexp  11722  ennnfoneleminc  11819  ennnfonelemkh  11820  ennnfonelemhf1o  11821  ennnfonelemhom  11823  setsn0fun  11891  restopnb  12245  restdis  12248  tgcnp  12273  cnntr  12289  cnsscnp  12293  txcn  12339  txlm  12343  mettri  12437  blssexps  12493  blssex  12494  mopni3  12548  metss  12558  2spim  12775
  Copyright terms: Public domain W3C validator