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

Theorem expcom 113
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 112 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
32com12 30 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  ancoms  259  syldan  270  sylan  271  pm4.79dc  820  dedlema  887  dedlemb  888  19.35-1  1531  cbval2  1812  cbvex2  1813  r19.21be  2427  r19.35-1  2477  mosubt  2740  sbcrext  2862  uneqdifeqim  3335  ssuni  3629  uniss2  3638  elpwuni  3768  elssabg  3929  elpw2g  3937  epelg  4054  elnn  4355  relop  4513  riinint  4620  cnviinm  4886  funopg  4961  fun  5090  tz6.12c  5230  fvelrnb  5248  fmptco  5357  fnressn  5376  fressnfv  5377  fvtp2g  5397  fvtp3g  5398  fconst2g  5403  isores3  5482  isoselem  5486  eloprabga  5618  fo1stresm  5815  poxp  5880  brtpos2  5896  smores  5937  tfrlem1  5953  tfrlemi1  5976  rdgon  6003  frecrdg  6022  freccl  6023  nnacl  6089  nnmcl  6090  nnacom  6093  nnaass  6094  nnmsucr  6097  nnmordi  6119  iinerm  6208  th3qlem2  6239  brdomg  6259  f1domg  6268  ssdomg  6288  nndomo  6356  carden2bex  6426  addclpi  6482  addnidpig  6491  genpassl  6679  genpassu  6680  nqprloc  6700  ltaprlem  6773  recexprlemopl  6780  recexprlemopu  6782  recexprlemupu  6783  recexprlemss1l  6790  recexprlemss1u  6791  cauappcvgprlemupu  6804  caucvgprlemupu  6827  caucvgprprlemupu  6855  archsr  6923  peano2nnnn  6986  receuap  7723  peano2nn  8001  nnaddcl  8009  zrevaddcl  8351  nzadd  8353  zdiv  8385  nneo  8399  zeo2  8402  peano5uzti  8404  fzind  8411  fnn0ind  8412  lbzbi  8647  qrevaddcl  8675  irradd  8677  irrmul  8678  ltsubrp  8714  ltaddrp  8715  icoshft  8958  fzen  9008  elfzm11  9054  uzsplit  9055  fzoval  9106  elfzom1elp1fzo  9159  modaddmodup  9331  frec2uzzd  9344  frec2uzrdg  9353  iseqss  9384  iseqfveq2  9386  iseqshft2  9390  monoord  9393  iseqsplit  9396  iseqcaopr3  9398  iseqid3s  9404  iseqhomo  9406  iseqz  9407  expadd  9456  expmul  9459  leexp1a  9469  faccl  9596  facdiv  9599  faclbnd  9602  faclbnd6  9605  shftlem  9638  resqrexlemover  9829  resqrexlemdecn  9831  resqrexlemlo  9832  resqrexlemcalc3  9835  climub  10087  climserile  10088  dvds2ln  10132  dvdsabseq  10151  dvdsdivcl  10154  alzdvds  10158  oddnn02np1  10184  m1exp1  10205  nn0o1gt2  10209  nno  10210  nn0seqcvgd  10235  ialginv  10241  ialgcvga  10245  ialgfx  10246  2spim  10265
  Copyright terms: Public domain W3C validator