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

Theorem impcom 124
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 123 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem is referenced by:  mpan9  279  19.41h  1648  19.41  1649  equtr2  1672  mopick  2055  2euex  2064  gencl  2692  2gencl  2693  rspccva  2762  indifdir  3302  sseq0  3374  minel  3394  r19.2m  3419  r19.2mOLD  3420  elelpwi  3492  ssuni  3728  disjiun  3894  trintssm  4012  ssexg  4037  pofun  4204  sowlin  4212  2optocl  4586  3optocl  4587  elrnmpt1  4760  resieq  4799  fnun  5199  fss  5254  fun  5265  dmfex  5282  fvelimab  5445  mptfvex  5474  fmptco  5554  fnressn  5574  fressnfv  5575  fvtp2g  5597  fvtp3g  5598  fnex  5610  funfvima3  5619  isores3  5684  f1o2ndf1  6093  reldmtpos  6118  smores  6157  tfrlem7  6182  tfrlemi1  6197  tfrexlem  6199  tfrcl  6229  frecrdg  6273  nnacl  6344  nnmcl  6345  nnmsucr  6352  nntri3or  6357  nnaword  6375  nnaordex  6391  2ecoptocl  6485  ssct  6680  enm  6682  xpf1o  6706  ac6sfi  6760  f1dmvrnfibi  6800  f1vrnfibi  6801  updjud  6935  enumct  6968  elni2  7090  ax1rid  7653  negf1o  8112  mulgt1  8589  lbreu  8671  nnaddcl  8708  nnmulcl  8709  zaddcllempos  9059  zaddcllemneg  9061  nn0n0n1ge2b  9098  fzind  9134  fnn0ind  9135  uzaddcl  9349  uzsubsubfz  9795  elfz1b  9838  elfz0ubfz0  9870  fz0fzdiffz0  9875  elfzmlbp  9877  fzofzim  9933  elfzom1elp1fzo  9947  elfzom1p1elfzo  9959  ssfzo12bi  9970  modfzo0difsn  10136  seq3val  10199  seqvalcd  10200  expcllem  10272  expap0  10291  faclbnd  10455  faclbnd6  10458  fihashf1rn  10503  omgadd  10516  hashfzp1  10538  seq3coll  10553  cjexp  10633  r19.29uz  10732  resqrexlemover  10750  resqrexlemlo  10753  resqrexlemcalc3  10756  absexp  10819  fimaxre2  10966  climshft  11041  climub  11081  climserle  11082  sumfct  11111  isumss2  11130  binom  11221  bcxmas  11226  demoivreALT  11407  dvdsdivcl  11475  dvdsfac  11485  oddnn02np1  11504  oddge22np1  11505  evennn02n  11506  evennn2n  11507  m1exp1  11525  nn0o  11531  flodddiv4  11558  gcdneg  11597  bezoutlemmain  11613  dfgcd2  11629  gcdmultiple  11635  alginv  11655  cncongr1  11711  prmdvdsexp  11753  prmndvdsfaclt  11761  clsss  12214  xmettri2  12457  mettri  12469  metss  12590  bdssexg  13029  bj-findis  13104  nninfalllemn  13129  nninfalllem1  13130  nninfsellemdc  13133
  Copyright terms: Public domain W3C validator