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  1663  19.41  1664  equtr2  1687  mopick  2077  2euex  2086  gencl  2718  2gencl  2719  rspccva  2788  indifdir  3332  sseq0  3404  minel  3424  r19.2m  3449  r19.2mOLD  3450  elelpwi  3522  ssuni  3758  disjiun  3924  trintssm  4042  ssexg  4067  pofun  4234  sowlin  4242  2optocl  4616  3optocl  4617  elrnmpt1  4790  resieq  4829  fnun  5229  fss  5284  fun  5295  dmfex  5312  fvelimab  5477  mptfvex  5506  fmptco  5586  fnressn  5606  fressnfv  5607  fvtp2g  5629  fvtp3g  5630  fnex  5642  funfvima3  5651  isores3  5716  f1o2ndf1  6125  reldmtpos  6150  smores  6189  tfrlem7  6214  tfrlemi1  6229  tfrexlem  6231  tfrcl  6261  frecrdg  6305  nnacl  6376  nnmcl  6377  nnmsucr  6384  nntri3or  6389  nnaword  6407  nnaordex  6423  2ecoptocl  6517  ssct  6712  enm  6714  xpf1o  6738  ac6sfi  6792  f1dmvrnfibi  6832  f1vrnfibi  6833  updjud  6967  enumct  7000  elni2  7134  ax1rid  7697  negf1o  8156  mulgt1  8633  lbreu  8715  nnaddcl  8752  nnmulcl  8753  zaddcllempos  9103  zaddcllemneg  9105  nn0n0n1ge2b  9142  fzind  9178  fnn0ind  9179  uzaddcl  9393  uzsubsubfz  9839  elfz1b  9882  elfz0ubfz0  9914  fz0fzdiffz0  9919  elfzmlbp  9921  fzofzim  9977  elfzom1elp1fzo  9991  elfzom1p1elfzo  10003  ssfzo12bi  10014  modfzo0difsn  10180  seq3val  10243  seqvalcd  10244  expcllem  10316  expap0  10335  faclbnd  10499  faclbnd6  10502  fihashf1rn  10547  omgadd  10560  hashfzp1  10582  seq3coll  10597  cjexp  10677  r19.29uz  10776  resqrexlemover  10794  resqrexlemlo  10797  resqrexlemcalc3  10800  absexp  10863  fimaxre2  11010  climshft  11085  climub  11125  climserle  11126  sumfct  11155  isumss2  11174  binom  11265  bcxmas  11270  clim2prod  11320  prodfap0  11326  prodfrecap  11327  demoivreALT  11491  dvdsdivcl  11559  dvdsfac  11569  oddnn02np1  11588  oddge22np1  11589  evennn02n  11590  evennn2n  11591  m1exp1  11609  nn0o  11615  flodddiv4  11642  gcdneg  11681  bezoutlemmain  11697  dfgcd2  11713  gcdmultiple  11719  alginv  11739  cncongr1  11795  prmdvdsexp  11837  prmndvdsfaclt  11845  clsss  12301  xmettri2  12544  mettri  12556  metss  12677  bdssexg  13186  bj-findis  13261  nninfalllemn  13288  nninfalllem1  13289  nninfsellemdc  13292
  Copyright terms: Public domain W3C validator