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

Theorem expcom 114
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 113 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 30 1  |-  ( ps 
->  ( ph  ->  ch ) )
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  1839  cbvex2  1840  nelelne  2341  r19.21be  2457  r19.35-1  2509  mosubt  2778  sbcrext  2900  uneqdifeqim  3344  ssuni  3643  uniss2  3652  elpwuni  3782  elssabg  3943  elpw2g  3951  epelg  4073  elnn  4374  relop  4534  riinint  4641  cnviinm  4909  funopg  4984  fun  5114  tz6.12c  5255  fvelrnb  5273  fmptco  5382  fnressn  5401  fressnfv  5402  fvtp2g  5422  fvtp3g  5423  fconst2g  5428  isores3  5506  isoselem  5510  eloprabga  5642  fo1stresm  5839  poxp  5904  brtpos2  5920  smores  5961  tfrlem1  5977  tfrlemi1  6001  tfr1onlemaccex  6017  tfrcllemaccex  6030  frecrdg  6077  oawordriexmid  6134  nnacl  6144  nnmcl  6145  nnacom  6148  nnaass  6149  nnmsucr  6152  nndifsnid  6167  nnmordi  6176  iinerm  6265  th3qlem2  6296  brdomg  6316  f1domg  6326  ssdomg  6346  nndomo  6420  carden2bex  6569  addclpi  6631  addnidpig  6640  genpassl  6828  genpassu  6829  nqprloc  6849  ltaprlem  6922  recexprlemopl  6929  recexprlemopu  6931  recexprlemupu  6932  recexprlemss1l  6939  recexprlemss1u  6940  cauappcvgprlemupu  6953  caucvgprlemupu  6976  caucvgprprlemupu  7004  archsr  7072  peano2nnnn  7135  receuap  7878  peano2nn  8170  nnaddcl  8178  zrevaddcl  8534  nzadd  8536  zdiv  8568  nneo  8583  zeo2  8586  peano5uzti  8588  fzind  8595  fnn0ind  8596  lbzbi  8834  qrevaddcl  8862  irradd  8864  irrmul  8865  ltsubrp  8901  ltaddrp  8902  icoshft  9140  fzen  9190  elfzm11  9236  uzsplit  9237  fzoval  9287  elfzom1elp1fzo  9340  exfzdc  9378  modaddmodup  9521  frec2uzrdg  9543  iseqoveq  9592  iseqss  9593  iseqsst  9594  iseqfveq2  9596  iseqshft2  9600  monoord  9603  iseqsplit  9606  iseqcaopr3  9608  iseqid3s  9614  iseqid2  9616  iseqhomo  9617  iseqz  9618  expadd  9667  expmul  9670  leexp1a  9680  faccl  9811  facdiv  9814  faclbnd  9817  faclbnd6  9820  omgadd  9878  hashunsng  9883  shftlem  9905  resqrexlemover  10097  resqrexlemdecn  10099  resqrexlemlo  10100  resqrexlemcalc3  10103  climub  10383  climserile  10384  dvds2ln  10436  dvdsabseq  10455  dvdsdivcl  10458  alzdvds  10462  oddnn02np1  10487  m1exp1  10508  nn0o1gt2  10512  nno  10513  ndvdsadd  10538  flodddiv4  10541  gcddiv  10615  gcdmultiple  10616  gcdmultiplez  10617  rplpwr  10623  dvdssq  10627  nn0seqcvgd  10630  ialginv  10636  ialgcvga  10640  ialgfx  10641  isprm2  10706  isprm3  10707  prmdvdsexp  10734  2spim  10837
  Copyright terms: Public domain W3C validator