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  1708  19.41  1709  equtr2  1734  mopick  2132  2euex  2141  gencl  2804  2gencl  2805  rspccva  2876  indifdir  3429  sseq0  3502  minel  3522  r19.2m  3547  r19.2mOLD  3548  elelpwi  3628  ssuni  3872  disjiun  4039  trintssm  4158  ssexg  4183  pofun  4359  sowlin  4367  2optocl  4752  3optocl  4753  elrnmpt1  4929  resieq  4969  fnun  5382  fss  5437  fun  5448  dmfex  5465  fvelimab  5635  mptfvex  5665  fmptco  5746  fnressn  5770  fressnfv  5771  fvtp2g  5793  fvtp3g  5794  fnex  5806  funfvima3  5818  isores3  5884  f1o2ndf1  6314  reldmtpos  6339  smores  6378  tfrlem7  6403  tfrlemi1  6418  tfrexlem  6420  tfrcl  6450  frecrdg  6494  nnacl  6566  nnmcl  6567  nnmsucr  6574  nntri3or  6579  nnaword  6597  nnaordex  6614  2ecoptocl  6710  ssct  6913  enm  6915  xpf1o  6941  ac6sfi  6995  f1dmvrnfibi  7046  f1vrnfibi  7047  updjud  7184  enumct  7217  nnnninfeq  7230  exmidontriimlem4  7336  exmidontriim  7337  elni2  7427  ax1rid  7990  negf1o  8454  mulgt1  8936  lbreu  9018  nnaddcl  9056  nnmulcl  9057  zaddcllempos  9409  zaddcllemneg  9411  nn0n0n1ge2b  9452  fzind  9488  fnn0ind  9489  uzaddcl  9707  elpq  9770  uzsubsubfz  10169  elfz1b  10212  elfz0ubfz0  10247  fz0fzdiffz0  10252  elfzmlbp  10254  fzofzim  10312  elfzom1elp1fzo  10331  elfzom1p1elfzo  10343  ssfzo12bi  10354  modfzo0difsn  10540  seq3val  10605  seqvalcd  10606  expcllem  10695  expap0  10714  apexp1  10863  faclbnd  10886  faclbnd6  10889  fihashf1rn  10933  omgadd  10947  hashfzp1  10969  seq3coll  10987  fundm2domnop0  10990  lswlgt0cl  11045  ccatsymb  11058  swrdnd  11112  swrd0g  11113  swrdspsleq  11120  cjexp  11204  r19.29uz  11303  resqrexlemover  11321  resqrexlemlo  11324  resqrexlemcalc3  11327  absexp  11390  fimaxre2  11538  climshft  11615  climub  11655  climserle  11656  sumfct  11685  isumss2  11704  binom  11795  bcxmas  11800  clim2prod  11850  prodfap0  11856  prodfrecap  11857  prodfct  11898  demoivreALT  12085  dvdsdivcl  12161  dvdsfac  12171  oddnn02np1  12191  oddge22np1  12192  evennn02n  12193  evennn2n  12194  m1exp1  12212  nn0o  12218  flodddiv4  12247  gcdneg  12303  bezoutlemmain  12319  dfgcd2  12335  gcdmultiple  12341  nnwosdc  12360  alginv  12369  cncongr1  12425  prmdvdsexp  12470  prmndvdsfaclt  12478  dfgrp2  13359  srgmulgass  13751  lmodvsmmulgdi  14085  lmodfopnelem1  14086  rmodislmodlem  14112  cnfldmulg  14338  cnfldexp  14339  clsss  14590  xmettri2  14833  mettri  14845  metss  14966  plycolemc  15230  zabsle1  15476  gausslemma2dlem1a  15535  gausslemma2dlem2  15539  gausslemma2dlem3  15540  gausslemma2dlem4  15541  2lgslem1a1  15563  bdssexg  15840  bj-findis  15915  nninfalllem1  15945  nninfsellemdc  15947  redc0  15996