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

Theorem expcom 115
Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
exp.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
expcom  |-  ( ps 
->  ( ph  ->  ch ) )

Proof of Theorem expcom
StepHypRef Expression
1 exp.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 114 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 30 1  |-  ( ps 
->  ( ph  ->  ch ) )
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  549  pm4.79dc  889  dedlema  954  dedlemb  955  19.35-1  1604  cbval2  1894  cbvex2  1895  nelelne  2401  r19.21be  2526  r19.35-1  2584  mosubt  2864  sbcrext  2989  uneqdifeqim  3452  ssuni  3765  uniss2  3774  elpwuni  3909  elssabg  4080  elpw2g  4088  epelg  4219  elnn  4526  relop  4696  riinint  4807  cnviinm  5087  funopg  5164  fun  5302  tz6.12c  5458  fvelrnb  5476  fmptco  5593  fnressn  5613  fressnfv  5614  fvtp2g  5636  fvtp3g  5637  fconst2g  5642  isores3  5723  isoselem  5728  eloprabga  5865  fo1stresm  6066  poxp  6136  brtpos2  6155  smores  6196  tfrlem1  6212  tfrlemi1  6236  tfr1onlemaccex  6252  tfrcllemaccex  6265  frecrdg  6312  oawordriexmid  6373  nnacl  6383  nnmcl  6384  nnacom  6387  nnaass  6388  nnmsucr  6391  nndifsnid  6410  nnmordi  6419  iinerm  6508  th3qlem2  6539  elpmg  6565  pmss12g  6576  mapsn  6591  brdomg  6649  f1domg  6659  ssdomg  6679  nndomo  6765  elfi2  6867  carden2bex  7061  cc3  7099  addclpi  7158  addnidpig  7167  genpassl  7355  genpassu  7356  nqprloc  7376  ltaprlem  7449  recexprlemopl  7456  recexprlemopu  7458  recexprlemupu  7459  recexprlemss1l  7466  recexprlemss1u  7467  cauappcvgprlemupu  7480  caucvgprlemupu  7503  caucvgprprlemupu  7531  archsr  7613  peano2nnnn  7684  receuap  8453  peano2nn  8755  nnaddcl  8763  zrevaddcl  9127  nzadd  9129  zdiv  9162  nneo  9177  zeo2  9180  peano5uzti  9182  fzind  9189  fnn0ind  9190  lbzbi  9434  qrevaddcl  9462  irradd  9464  irrmul  9465  ltsubrp  9506  ltaddrp  9507  xnn0xadd0  9679  icoshft  9802  fzen  9853  elfzm11  9901  uzsplit  9902  fzoval  9955  elfzom1elp1fzo  10009  exfzdc  10047  modaddmodup  10190  frec2uzrdg  10212  seq3clss  10270  monoord  10279  seq3caopr3  10284  seq3f1olemp  10305  seq3id3  10310  seq3homo  10313  seq3z  10314  ser3ge0  10320  expadd  10365  expmul  10368  leexp1a  10378  faccl  10512  facdiv  10515  faclbnd  10518  faclbnd6  10521  omgadd  10579  hashunsng  10584  seq3coll  10616  shftlem  10619  resqrexlemover  10813  resqrexlemdecn  10815  resqrexlemlo  10816  resqrexlemcalc3  10819  climub  11144  climserle  11145  fsumzcl2  11205  fsumsplitsnun  11219  fsum2d  11235  modfsummodlemstep  11257  fsumabs  11265  fsumiun  11277  bcxmas  11289  cvgratnnlemnexp  11324  cvgratnnlemmn  11325  prodfap0  11345  prodfrecap  11346  ntrivcvgap  11348  prodmodc  11378  dvds2ln  11560  dvdsabseq  11579  dvdsdivcl  11582  alzdvds  11586  oddnn02np1  11611  m1exp1  11632  nn0o1gt2  11636  nno  11637  ndvdsadd  11662  flodddiv4  11665  gcddiv  11741  gcdmultiple  11742  gcdmultiplez  11743  rplpwr  11749  dvdssq  11753  nn0seqcvgd  11756  alginv  11762  algcvga  11766  algfx  11767  isprm2  11832  isprm3  11833  prmdvdsexp  11860  ennnfoneleminc  11958  ennnfonelemkh  11959  ennnfonelemhf1o  11960  ennnfonelemhom  11962  omiunct  11991  setsn0fun  12033  restopnb  12387  restdis  12390  tgcnp  12415  cnntr  12431  cnsscnp  12435  txcn  12481  txlm  12485  mettri  12579  blssexps  12635  blssex  12636  mopni3  12690  metss  12700  2spim  13142
  Copyright terms: Public domain W3C validator