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  802  dedlema  864  dedlemb  865  19.35-1  1497  cbval2  1778  cbvex2  1779  r19.21be  2388  r19.35-1  2438  mosubt  2695  uneqdifeqim  3285  ssuni  3576  uniss2  3585  elpwuni  3715  elssabg  3876  elpw2g  3884  epelg  4001  elnn  4255  relop  4413  riinint  4520  cnviinm  4786  funopg  4860  fun  4988  tz6.12c  5128  fvelrnb  5146  fmptco  5255  fnressn  5274  fressnfv  5275  fvtp2g  5295  fvtp3g  5296  fconst2g  5301  isores3  5380  isoselem  5384  eloprabga  5514  fo1stresm  5711  poxp  5775  brtpos2  5788  smores  5829  tfrlem1  5845  tfrlemi1  5867  rdgon  5893  frecrdg  5908  nnacl  5974  nnmcl  5975  nnacom  5978  nnaass  5979  nnmsucr  5982  nnmordi  6000  iinerm  6089  th3qlem2  6120  addclpi  6187  addnidpig  6196  genpassl  6379  genpassu  6380  nqprloc  6400  ltaprlem  6454  recexprlemopl  6459  recexprlemopu  6461  recexprlemupu  6462  recexprlemss1l  6469  recexprlemss1u  6470  2spim  7013
  Copyright terms: Public domain W3C validator