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

Theorem impcom 125
Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
imp.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
impcom  |-  ( ( ps  /\  ph )  ->  ch )

Proof of Theorem impcom
StepHypRef Expression
1 imp.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21com12 30 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
32imp 124 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem is referenced by:  mpan9  281  19.41h  1683  19.41  1684  equtr2  1709  mopick  2102  2euex  2111  gencl  2767  2gencl  2768  rspccva  2838  indifdir  3389  sseq0  3462  minel  3482  r19.2m  3507  r19.2mOLD  3508  elelpwi  3584  ssuni  3827  disjiun  3993  trintssm  4112  ssexg  4137  pofun  4306  sowlin  4314  2optocl  4697  3optocl  4698  elrnmpt1  4871  resieq  4910  fnun  5314  fss  5369  fun  5380  dmfex  5397  fvelimab  5564  mptfvex  5593  fmptco  5674  fnressn  5694  fressnfv  5695  fvtp2g  5717  fvtp3g  5718  fnex  5730  funfvima3  5741  isores3  5806  f1o2ndf1  6219  reldmtpos  6244  smores  6283  tfrlem7  6308  tfrlemi1  6323  tfrexlem  6325  tfrcl  6355  frecrdg  6399  nnacl  6471  nnmcl  6472  nnmsucr  6479  nntri3or  6484  nnaword  6502  nnaordex  6519  2ecoptocl  6613  ssct  6808  enm  6810  xpf1o  6834  ac6sfi  6888  f1dmvrnfibi  6933  f1vrnfibi  6934  updjud  7071  enumct  7104  nnnninfeq  7116  exmidontriimlem4  7213  exmidontriim  7214  elni2  7288  ax1rid  7851  negf1o  8313  mulgt1  8791  lbreu  8873  nnaddcl  8910  nnmulcl  8911  zaddcllempos  9261  zaddcllemneg  9263  nn0n0n1ge2b  9303  fzind  9339  fnn0ind  9340  uzaddcl  9557  elpq  9619  uzsubsubfz  10015  elfz1b  10058  elfz0ubfz0  10093  fz0fzdiffz0  10098  elfzmlbp  10100  fzofzim  10156  elfzom1elp1fzo  10170  elfzom1p1elfzo  10182  ssfzo12bi  10193  modfzo0difsn  10363  seq3val  10426  seqvalcd  10427  expcllem  10499  expap0  10518  apexp1  10664  faclbnd  10687  faclbnd6  10690  fihashf1rn  10735  omgadd  10749  hashfzp1  10771  seq3coll  10789  cjexp  10869  r19.29uz  10968  resqrexlemover  10986  resqrexlemlo  10989  resqrexlemcalc3  10992  absexp  11055  fimaxre2  11202  climshft  11279  climub  11319  climserle  11320  sumfct  11349  isumss2  11368  binom  11459  bcxmas  11464  clim2prod  11514  prodfap0  11520  prodfrecap  11521  prodfct  11562  demoivreALT  11748  dvdsdivcl  11822  dvdsfac  11832  oddnn02np1  11851  oddge22np1  11852  evennn02n  11853  evennn2n  11854  m1exp1  11872  nn0o  11878  flodddiv4  11905  gcdneg  11949  bezoutlemmain  11965  dfgcd2  11981  gcdmultiple  11987  nnwosdc  12006  alginv  12013  cncongr1  12069  prmdvdsexp  12114  prmndvdsfaclt  12122  dfgrp2  12762  srgmulgass  12965  clsss  13111  xmettri2  13354  mettri  13366  metss  13487  zabsle1  13893  bdssexg  14138  bj-findis  14213  nninfalllem1  14240  nninfsellemdc  14242  redc0  14288
  Copyright terms: Public domain W3C validator