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  1685  19.41  1686  equtr2  1711  mopick  2104  2euex  2113  gencl  2770  2gencl  2771  rspccva  2841  indifdir  3392  sseq0  3465  minel  3485  r19.2m  3510  r19.2mOLD  3511  elelpwi  3588  ssuni  3832  disjiun  3999  trintssm  4118  ssexg  4143  pofun  4313  sowlin  4321  2optocl  4704  3optocl  4705  elrnmpt1  4879  resieq  4918  fnun  5323  fss  5378  fun  5389  dmfex  5406  fvelimab  5573  mptfvex  5602  fmptco  5683  fnressn  5703  fressnfv  5704  fvtp2g  5726  fvtp3g  5727  fnex  5739  funfvima3  5751  isores3  5816  f1o2ndf1  6229  reldmtpos  6254  smores  6293  tfrlem7  6318  tfrlemi1  6333  tfrexlem  6335  tfrcl  6365  frecrdg  6409  nnacl  6481  nnmcl  6482  nnmsucr  6489  nntri3or  6494  nnaword  6512  nnaordex  6529  2ecoptocl  6623  ssct  6818  enm  6820  xpf1o  6844  ac6sfi  6898  f1dmvrnfibi  6943  f1vrnfibi  6944  updjud  7081  enumct  7114  nnnninfeq  7126  exmidontriimlem4  7223  exmidontriim  7224  elni2  7313  ax1rid  7876  negf1o  8339  mulgt1  8820  lbreu  8902  nnaddcl  8939  nnmulcl  8940  zaddcllempos  9290  zaddcllemneg  9292  nn0n0n1ge2b  9332  fzind  9368  fnn0ind  9369  uzaddcl  9586  elpq  9648  uzsubsubfz  10047  elfz1b  10090  elfz0ubfz0  10125  fz0fzdiffz0  10130  elfzmlbp  10132  fzofzim  10188  elfzom1elp1fzo  10202  elfzom1p1elfzo  10214  ssfzo12bi  10225  modfzo0difsn  10395  seq3val  10458  seqvalcd  10459  expcllem  10531  expap0  10550  apexp1  10698  faclbnd  10721  faclbnd6  10724  fihashf1rn  10768  omgadd  10782  hashfzp1  10804  seq3coll  10822  cjexp  10902  r19.29uz  11001  resqrexlemover  11019  resqrexlemlo  11022  resqrexlemcalc3  11025  absexp  11088  fimaxre2  11235  climshft  11312  climub  11352  climserle  11353  sumfct  11382  isumss2  11401  binom  11492  bcxmas  11497  clim2prod  11547  prodfap0  11553  prodfrecap  11554  prodfct  11595  demoivreALT  11781  dvdsdivcl  11856  dvdsfac  11866  oddnn02np1  11885  oddge22np1  11886  evennn02n  11887  evennn2n  11888  m1exp1  11906  nn0o  11912  flodddiv4  11939  gcdneg  11983  bezoutlemmain  11999  dfgcd2  12015  gcdmultiple  12021  nnwosdc  12040  alginv  12047  cncongr1  12103  prmdvdsexp  12148  prmndvdsfaclt  12156  dfgrp2  12902  srgmulgass  13172  lmodvsmmulgdi  13413  lmodfopnelem1  13414  rmodislmodlem  13440  cnfldmulg  13473  cnfldexp  13474  clsss  13621  xmettri2  13864  mettri  13876  metss  13997  zabsle1  14403  bdssexg  14659  bj-findis  14734  nninfalllem1  14760  nninfsellemdc  14762  redc0  14808