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  6506  genpassu  6507  nqprloc  6527  ltaprlem  6590  recexprlemopl  6596  recexprlemopu  6598  recexprlemupu  6599  recexprlemss1l  6606  recexprlemss1u  6607  cauappcvgprlemupu  6620  archsr  6688  receuap  7412  peano2nn  7687  nnaddcl  7695  zrevaddcl  8051  zdiv  8084  nneo  8097  zeo2  8100  peano5uzti  8102  fzind  8109  fnn0ind  8110  lbzbi  8307  qrevaddcl  8333  irradd  8335  irrmul  8336  ltsubrp  8372  ltaddrp  8373  icoshft  8608  fzen  8657  elfzm11  8703  uzsplit  8704  fzoval  8755  elfzom1elp1fzo  8808  frec2uzzd  8847  frec2uzrdg  8856  iseqfveq2  8885  expadd  8931  expmul  8934  leexp1a  8943  2spim  9221
  Copyright terms: Public domain W3C validator