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  280  sylan  281  animpimp2impd  533  pm4.79dc  873  dedlema  938  dedlemb  939  19.35-1  1588  cbval2  1873  cbvex2  1874  nelelne  2377  r19.21be  2500  r19.35-1  2558  mosubt  2834  sbcrext  2958  uneqdifeqim  3418  ssuni  3728  uniss2  3737  elpwuni  3872  elssabg  4043  elpw2g  4051  epelg  4182  elnn  4489  relop  4659  riinint  4770  cnviinm  5050  funopg  5127  fun  5265  tz6.12c  5419  fvelrnb  5437  fmptco  5554  fnressn  5574  fressnfv  5575  fvtp2g  5597  fvtp3g  5598  fconst2g  5603  isores3  5684  isoselem  5689  eloprabga  5826  fo1stresm  6027  poxp  6097  brtpos2  6116  smores  6157  tfrlem1  6173  tfrlemi1  6197  tfr1onlemaccex  6213  tfrcllemaccex  6226  frecrdg  6273  oawordriexmid  6334  nnacl  6344  nnmcl  6345  nnacom  6348  nnaass  6349  nnmsucr  6352  nndifsnid  6371  nnmordi  6380  iinerm  6469  th3qlem2  6500  elpmg  6526  pmss12g  6537  mapsn  6552  brdomg  6610  f1domg  6620  ssdomg  6640  nndomo  6726  elfi2  6828  carden2bex  7013  addclpi  7103  addnidpig  7112  genpassl  7300  genpassu  7301  nqprloc  7321  ltaprlem  7394  recexprlemopl  7401  recexprlemopu  7403  recexprlemupu  7404  recexprlemss1l  7411  recexprlemss1u  7412  cauappcvgprlemupu  7425  caucvgprlemupu  7448  caucvgprprlemupu  7476  archsr  7558  peano2nnnn  7629  receuap  8397  peano2nn  8696  nnaddcl  8704  zrevaddcl  9062  nzadd  9064  zdiv  9097  nneo  9112  zeo2  9115  peano5uzti  9117  fzind  9124  fnn0ind  9125  lbzbi  9364  qrevaddcl  9392  irradd  9394  irrmul  9395  ltsubrp  9433  ltaddrp  9434  xnn0xadd0  9605  icoshft  9728  fzen  9778  elfzm11  9826  uzsplit  9827  fzoval  9880  elfzom1elp1fzo  9934  exfzdc  9972  modaddmodup  10115  frec2uzrdg  10137  seq3clss  10195  monoord  10204  seq3caopr3  10209  seq3f1olemp  10230  seq3id3  10235  seq3homo  10238  seq3z  10239  ser3ge0  10245  expadd  10290  expmul  10293  leexp1a  10303  faccl  10436  facdiv  10439  faclbnd  10442  faclbnd6  10445  omgadd  10503  hashunsng  10508  seq3coll  10540  shftlem  10543  resqrexlemover  10737  resqrexlemdecn  10739  resqrexlemlo  10740  resqrexlemcalc3  10743  climub  11068  climserle  11069  fsumzcl2  11129  fsumsplitsnun  11143  fsum2d  11159  modfsummodlemstep  11181  fsumabs  11189  fsumiun  11201  bcxmas  11213  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  dvds2ln  11438  dvdsabseq  11457  dvdsdivcl  11460  alzdvds  11464  oddnn02np1  11489  m1exp1  11510  nn0o1gt2  11514  nno  11515  ndvdsadd  11540  flodddiv4  11543  gcddiv  11619  gcdmultiple  11620  gcdmultiplez  11621  rplpwr  11627  dvdssq  11631  nn0seqcvgd  11634  alginv  11640  algcvga  11644  algfx  11645  isprm2  11710  isprm3  11711  prmdvdsexp  11738  ennnfoneleminc  11835  ennnfonelemkh  11836  ennnfonelemhf1o  11837  ennnfonelemhom  11839  setsn0fun  11907  restopnb  12261  restdis  12264  tgcnp  12289  cnntr  12305  cnsscnp  12309  txcn  12355  txlm  12359  mettri  12453  blssexps  12509  blssex  12510  mopni3  12564  metss  12574  2spim  12869
  Copyright terms: Public domain W3C validator