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  6591  recexprlemopl  6597  recexprlemopu  6599  recexprlemupu  6600  recexprlemss1l  6607  recexprlemss1u  6608  cauappcvgprlemupu  6621  caucvgprlemupu  6643  archsr  6708  receuap  7432  peano2nn  7707  nnaddcl  7715  zrevaddcl  8071  zdiv  8104  nneo  8117  zeo2  8120  peano5uzti  8122  fzind  8129  fnn0ind  8130  lbzbi  8327  qrevaddcl  8353  irradd  8355  irrmul  8356  ltsubrp  8392  ltaddrp  8393  icoshft  8628  fzen  8677  elfzm11  8723  uzsplit  8724  fzoval  8775  elfzom1elp1fzo  8828  frec2uzzd  8867  frec2uzrdg  8876  iseqfveq2  8905  expadd  8951  expmul  8954  leexp1a  8963  2spim  9241
  Copyright terms: Public domain W3C validator