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

Theorem expcom 116
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 115 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 30 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  ancoms  268  syldan  282  sylan  283  animpimp2impd  559  pm4.79dc  903  dedlema  969  dedlemb  970  19.35-1  1624  cbval2  1921  cbvex2  1922  nelelne  2439  r19.21be  2568  r19.35-1  2627  mosubt  2914  sbcrext  3040  uneqdifeqim  3508  ssuni  3829  uniss2  3838  elpwuni  3973  elssabg  4145  elpw2g  4153  epelg  4286  elomssom  4600  relop  4772  riinint  4883  cnviinm  5165  funopg  5245  fun  5383  tz6.12c  5540  fvelrnb  5558  fmptco  5677  fnressn  5697  fressnfv  5698  fvtp2g  5720  fvtp3g  5721  fconst2g  5726  isores3  5809  isoselem  5814  eloprabga  5955  fo1stresm  6155  poxp  6226  brtpos2  6245  smores  6286  tfrlem1  6302  tfrlemi1  6326  tfr1onlemaccex  6342  tfrcllemaccex  6355  frecrdg  6402  oawordriexmid  6464  nnacl  6474  nnmcl  6475  nnacom  6478  nnaass  6479  nnmsucr  6482  nndifsnid  6501  nnmordi  6510  iinerm  6600  th3qlem2  6631  elpmg  6657  pmss12g  6668  mapsn  6683  brdomg  6741  f1domg  6751  ssdomg  6771  nndomo  6857  elfi2  6964  nnnninfeq2  7120  carden2bex  7181  cc3  7245  addclpi  7304  addnidpig  7313  genpassl  7501  genpassu  7502  nqprloc  7522  ltaprlem  7595  recexprlemopl  7602  recexprlemopu  7604  recexprlemupu  7605  recexprlemss1l  7612  recexprlemss1u  7613  cauappcvgprlemupu  7626  caucvgprlemupu  7649  caucvgprprlemupu  7677  archsr  7759  peano2nnnn  7830  receuap  8602  peano2nn  8907  nnaddcl  8915  zrevaddcl  9279  nzadd  9281  zdiv  9317  nneo  9332  zeo2  9335  peano5uzti  9337  fzind  9344  fnn0ind  9345  lbzbi  9592  qrevaddcl  9620  irradd  9622  irrmul  9623  ltsubrp  9664  ltaddrp  9665  xnn0xadd0  9841  icoshft  9964  fzen  10016  elfzm11  10064  uzsplit  10065  fzoval  10121  elfzom1elp1fzo  10175  exfzdc  10213  modaddmodup  10360  frec2uzrdg  10382  seq3clss  10440  monoord  10449  seq3caopr3  10454  seq3f1olemp  10475  seq3id3  10480  seq3homo  10483  seq3z  10484  ser3ge0  10490  expadd  10535  expmul  10538  leexp1a  10548  modqexp  10619  faccl  10686  facdiv  10689  faclbnd  10692  faclbnd6  10695  omgadd  10753  hashunsng  10758  seq3coll  10793  shftlem  10796  resqrexlemover  10990  resqrexlemdecn  10992  resqrexlemlo  10993  resqrexlemcalc3  10996  climub  11323  climserle  11324  fsumzcl2  11384  fsumsplitsnun  11398  fsum2d  11414  modfsummodlemstep  11436  fsumabs  11444  fsumiun  11456  bcxmas  11468  cvgratnnlemnexp  11503  cvgratnnlemmn  11504  prodfap0  11524  prodfrecap  11525  ntrivcvgap  11527  prodmodc  11557  fprodssdc  11569  fprodabs  11595  fprod2d  11602  dvdsmod0  11771  dvds2ln  11802  dvdsabseq  11823  dvdsdivcl  11826  alzdvds  11830  oddnn02np1  11855  m1exp1  11876  nn0o1gt2  11880  nno  11881  ndvdsadd  11906  flodddiv4  11909  gcddiv  11990  gcdmultiple  11991  gcdmultiplez  11992  rplpwr  11998  dvdssq  12002  nn0seqcvgd  12011  alginv  12017  algcvga  12021  algfx  12022  isprm2  12087  isprm3  12088  prmdvdsexp  12118  eulerthlemrprm  12199  eulerthlema  12200  pcmpt  12311  ennnfoneleminc  12382  ennnfonelemkh  12383  ennnfonelemhf1o  12384  ennnfonelemhom  12386  omiunct  12415  nninfdclemlt  12422  setsn0fun  12469  mgmcl  12657  dfgrp3mlem  12844  mhmmulg  12899  srgpcomp  12986  restopnb  13314  restdis  13317  tgcnp  13342  cnntr  13358  cnsscnp  13362  txcn  13408  txlm  13412  mettri  13506  blssexps  13562  blssex  13563  mopni3  13617  metss  13627  2spim  14140
  Copyright terms: Public domain W3C validator