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

Theorem expcom 109
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 108 . 2 (φ → (ψχ))
32com12 27 1 (ψ → (φχ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  ancoms  255  syldan  266  sylan  267  pm4.79dc  808  dedlema  875  dedlemb  876  19.35-1  1512  cbval2  1793  cbvex2  1794  r19.21be  2404  r19.35-1  2454  mosubt  2712  uneqdifeqim  3302  ssuni  3593  uniss2  3602  elpwuni  3732  elssabg  3893  elpw2g  3901  epelg  4018  elnn  4271  relop  4429  riinint  4536  cnviinm  4802  funopg  4877  fun  5006  tz6.12c  5146  fvelrnb  5164  fmptco  5273  fnressn  5292  fressnfv  5293  fvtp2g  5313  fvtp3g  5314  fconst2g  5319  isores3  5398  isoselem  5402  eloprabga  5533  fo1stresm  5730  poxp  5794  brtpos2  5807  smores  5848  tfrlem1  5864  tfrlemi1  5887  rdgon  5913  frecrdg  5931  freccl  5932  nnacl  5998  nnmcl  5999  nnacom  6002  nnaass  6003  nnmsucr  6006  nnmordi  6025  iinerm  6114  th3qlem2  6145  brdomg  6165  f1domg  6174  ssdomg  6194  addclpi  6311  addnidpig  6320  genpassl  6507  genpassu  6508  nqprloc  6528  ltaprlem  6589  recexprlemopl  6595  recexprlemopu  6597  recexprlemupu  6598  recexprlemss1l  6605  recexprlemss1u  6606  archsr  6668  receuap  7392  peano2nn  7667  nnaddcl  7675  zrevaddcl  8031  zdiv  8064  nneo  8077  zeo2  8080  peano5uzti  8082  fzind  8089  fnn0ind  8090  lbzbi  8287  qrevaddcl  8313  irradd  8315  irrmul  8316  ltsubrp  8352  ltaddrp  8353  icoshft  8588  fzen  8637  elfzm11  8683  uzsplit  8684  fzoval  8735  elfzom1elp1fzo  8788  frec2uzzd  8827  frec2uzrdg  8836  iseqfveq2  8865  expadd  8911  expmul  8914  leexp1a  8923  2spim  9175
  Copyright terms: Public domain W3C validator