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

Theorem impcom 123
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 122 1  |-  ( ( ps  /\  ph )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem is referenced by:  mpan9  275  19.41h  1616  19.41  1617  equtr2  1638  mopick  2020  2euex  2029  gencl  2632  2gencl  2633  rspccva  2701  indifdir  3227  sseq0  3292  minel  3312  r19.2m  3336  elelpwi  3401  ssuni  3631  trintssm  3899  ssexg  3925  pofun  4075  sowlin  4083  2optocl  4443  3optocl  4444  elrnmpt1  4613  resieq  4650  fnun  5036  fss  5085  fun  5094  dmfex  5110  fvelimab  5261  mptfvex  5288  fmptco  5362  fnressn  5381  fressnfv  5382  fvtp2g  5402  fvtp3g  5403  fnex  5415  funfvima3  5424  isores3  5486  f1o2ndf1  5880  reldmtpos  5902  smores  5941  tfrlem7  5966  tfrlemi1  5981  tfrexlem  5983  tfrcl  6013  frecrdg  6057  nnacl  6124  nnmcl  6125  nnmsucr  6132  nntri3or  6137  nnaword  6150  nnaordex  6166  2ecoptocl  6260  ssct  6362  enm  6364  xpf1o  6385  ac6sfi  6431  f1dmvrnfibi  6452  f1vrnfibi  6453  elni2  6566  ax1rid  7105  negf1o  7553  mulgt1  8008  lbreu  8090  nnaddcl  8126  nnmulcl  8127  zaddcllempos  8469  zaddcllemneg  8471  nn0n0n1ge2b  8508  fzind  8543  fnn0ind  8544  uzaddcl  8755  uzsubsubfz  9142  elfz1b  9183  elfz0ubfz0  9213  fz0fzdiffz0  9218  elfzmlbp  9220  fzofzim  9274  elfzom1elp1fzo  9288  elfzom1p1elfzo  9300  ssfzo12bi  9311  modfzo0difsn  9477  iseqvalt  9532  iseqoveq  9540  iseqss  9541  iseqsst  9542  expivallem  9574  expcllem  9584  expap0  9603  faclbnd  9765  faclbnd6  9768  sizef1rn  9813  omgadd  9826  cjexp  9918  r19.29uz  10016  resqrexlemover  10034  resqrexlemlo  10037  resqrexlemcalc3  10040  absexp  10103  fimaxre2  10247  climshft  10281  climub  10320  climserile  10321  dvdsdivcl  10395  dvdsfac  10405  oddnn02np1  10424  oddge22np1  10425  evennn02n  10426  evennn2n  10427  m1exp1  10445  nn0o  10451  flodddiv4  10478  gcdneg  10517  bezoutlemmain  10531  dfgcd2  10547  gcdmultiple  10553  ialginv  10573  cncongr1  10629  prmdvdsexp  10671  prmndvdsfaclt  10679  bdssexg  10853  bj-findis  10932
  Copyright terms: Public domain W3C validator