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

Step	Hyp	Ref	Expression
1		imp.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	com12 30	. 2 |- ( ps -> ( ph -> ch ) )
3	2	imp 124	1 |- ( ( ps /\ ph ) -> ch )

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  1699  19.41  1700  equtr2  1725  mopick  2123  2euex  2132  gencl  2795  2gencl  2796  rspccva  2867  indifdir  3420  sseq0  3493  minel  3513  r19.2m  3538  r19.2mOLD  3539  elelpwi  3618  ssuni  3862  disjiun  4029  trintssm  4148  ssexg  4173  pofun  4348  sowlin  4356  2optocl  4741  3optocl  4742  elrnmpt1  4918  resieq  4957  fnun  5365  fss  5420  fun  5431  dmfex  5448  fvelimab  5618  mptfvex  5648  fmptco  5729  fnressn  5749  fressnfv  5750  fvtp2g  5772  fvtp3g  5773  fnex  5785  funfvima3  5797  isores3  5863  f1o2ndf1  6287  reldmtpos  6312  smores  6351  tfrlem7  6376  tfrlemi1  6391  tfrexlem  6393  tfrcl  6423  frecrdg  6467  nnacl  6539  nnmcl  6540  nnmsucr  6547  nntri3or  6552  nnaword  6570  nnaordex  6587  2ecoptocl  6683  ssct  6878  enm  6880  xpf1o  6906  ac6sfi  6960  f1dmvrnfibi  7011  f1vrnfibi  7012  updjud  7149  enumct  7182  nnnninfeq  7195  exmidontriimlem4  7293  exmidontriim  7294  elni2  7383  ax1rid  7946  negf1o  8410  mulgt1  8892  lbreu  8974  nnaddcl  9012  nnmulcl  9013  zaddcllempos  9365  zaddcllemneg  9367  nn0n0n1ge2b  9407  fzind  9443  fnn0ind  9444  uzaddcl  9662  elpq  9725  uzsubsubfz  10124  elfz1b  10167  elfz0ubfz0  10202  fz0fzdiffz0  10207  elfzmlbp  10209  fzofzim  10266  elfzom1elp1fzo  10280  elfzom1p1elfzo  10292  ssfzo12bi  10303  modfzo0difsn  10489  seq3val  10554  seqvalcd  10555  expcllem  10644  expap0  10663  apexp1  10812  faclbnd  10835  faclbnd6  10838  fihashf1rn  10882  omgadd  10896  hashfzp1  10918  seq3coll  10936  cjexp  11060  r19.29uz  11159  resqrexlemover  11177  resqrexlemlo  11180  resqrexlemcalc3  11183  absexp  11246  fimaxre2  11394  climshft  11471  climub  11511  climserle  11512  sumfct  11541  isumss2  11560  binom  11651  bcxmas  11656  clim2prod  11706  prodfap0  11712  prodfrecap  11713  prodfct  11754  demoivreALT  11941  dvdsdivcl  12017  dvdsfac  12027  oddnn02np1  12047  oddge22np1  12048  evennn02n  12049  evennn2n  12050  m1exp1  12068  nn0o  12074  flodddiv4  12103  gcdneg  12159  bezoutlemmain  12175  dfgcd2  12191  gcdmultiple  12197  nnwosdc  12216  alginv  12225  cncongr1  12281  prmdvdsexp  12326  prmndvdsfaclt  12334  dfgrp2  13169  srgmulgass  13555  lmodvsmmulgdi  13889  lmodfopnelem1  13890  rmodislmodlem  13916  cnfldmulg  14142  cnfldexp  14143  clsss  14364  xmettri2  14607  mettri  14619  metss  14740  plycolemc  15004  zabsle1  15250  gausslemma2dlem1a  15309  gausslemma2dlem2  15313  gausslemma2dlem3  15314  gausslemma2dlem4  15315  2lgslem1a1  15337  bdssexg  15560  bj-findis  15635  nninfalllem1  15662  nninfsellemdc  15664  redc0  15711