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  1733  19.41  1734  equtr2  1759  mopick  2161  2euex  2170  gencl  2848  2gencl  2849  vtocl4g  2888  vtocl4ga  2889  rspccva  2922  indifdir  3479  sseq0  3552  minel  3572  r19.2m  3598  r19.2mOLD  3599  elelpwi  3683  ssuni  3938  disjiun  4106  trintssm  4226  ssexg  4251  pofun  4435  sowlin  4443  2optocl  4829  3optocl  4830  ssrelrn  4949  elrnmpt1  5010  resieq  5050  fnun  5466  fss  5523  fun  5538  dmfex  5559  fvelimab  5735  mptfvex  5765  fmptco  5845  fnressn  5872  fressnfv  5873  fvtp2g  5895  fvtp3g  5896  fnex  5908  funfvima3  5922  isores3  5990  f1o2ndf1  6426  funsssuppss  6460  reldmtpos  6486  smores  6525  tfrlem7  6550  tfrlemi1  6565  tfrexlem  6567  tfrcl  6597  frecrdg  6641  nnacl  6715  nnmcl  6716  nnmsucr  6723  nntri3or  6728  nnaword  6746  nnaordex  6763  2ecoptocl  6859  ssct  7069  enm  7073  xpf1o  7099  ac6sfi  7157  f1dmvrnfibi  7213  f1vrnfibi  7214  suppeqfsuppbi  7250  updjud  7375  enumct  7408  nnnninfeq  7421  exmidontriimlem4  7533  exmidontriim  7534  elni2  7631  ax1rid  8194  negf1o  8657  mulgt1  9139  lbreu  9221  nnaddcl  9259  nnmulcl  9260  zaddcllempos  9616  zaddcllemneg  9618  nn0n0n1ge2b  9660  fzind  9696  fnn0ind  9697  uzaddcl  9921  elpq  9984  uzsubsubfz  10384  elfz1b  10428  elfz0ubfz0  10463  fz0fzdiffz0  10468  elfzmlbp  10470  fzofzim  10531  elfzom1elp1fzo  10551  elfzom1p1elfzo  10563  ssfzo12bi  10574  modfzo0difsn  10761  seq3val  10826  seqvalcd  10827  expcllem  10916  expap0  10935  apexp1  11084  faclbnd  11107  faclbnd6  11110  fihashf1rn  11155  omgadd  11170  hashfzp1  11193  hashmap  11196  seq3coll  11218  fundm2domnop0  11224  lswlgt0cl  11281  ccatsymb  11294  swrdnd  11355  swrd0g  11356  swrdspsleq  11363  pfxsuff1eqwrdeq  11395  swrdswrdlem  11400  swrdswrd  11401  wrd2ind  11419  pfxccatin12lem2a  11423  swrdccatin2  11425  pfxccatin12lem2  11427  pfxccatin12lem3  11428  pfxccatin12  11429  pfxccat3  11430  swrdccat  11431  pfxccat3a  11434  swrdccat3blem  11435  cjexp  11582  r19.29uz  11681  resqrexlemover  11699  resqrexlemlo  11702  resqrexlemcalc3  11705  absexp  11768  fimaxre2  11916  climshft  11993  climub  12033  climserle  12034  sumfct  12063  isumss2  12083  binom  12174  bcxmas  12179  clim2prod  12229  prodfap0  12235  prodfrecap  12236  prodfct  12277  demoivreALT  12464  dvdsdivcl  12540  dvdsfac  12550  oddnn02np1  12570  oddge22np1  12571  evennn02n  12572  evennn2n  12573  m1exp1  12591  nn0o  12597  flodddiv4  12626  gcdneg  12682  bezoutlemmain  12698  dfgcd2  12714  gcdmultiple  12720  nnwosdc  12739  alginv  12748  cncongr1  12804  prmdvdsexp  12849  prmndvdsfaclt  12857  dfgrp2  13757  srgmulgass  14150  lmodvsmmulgdi  14488  lmodfopnelem1  14489  rmodislmodlem  14515  cnfldmulg  14741  cnfldexp  14742  clsss  15000  xmettri2  15243  mettri  15255  metss  15376  plycolemc  15640  zabsle1  15889  gausslemma2dlem1a  15948  gausslemma2dlem2  15952  gausslemma2dlem3  15953  gausslemma2dlem4  15954  2lgslem1a1  15976  incistruhgr  16102  umgrislfupgrenlem  16142  uhgr2edg  16218  usgredg2vlem2  16235  subgrfun  16279  wlkl1loop  16370  wlkres  16391  clwwlkccatlem  16412  isclwwlknx  16428  clwwlkext2edg  16434  clwwlknonel  16444  clwwlknonex2lem2  16450  clwwlknun  16453  depindlem2  16519  depindlem3  16520  bdssexg  16691  bj-findis  16766  nninfalllem1  16803  nninfsellemdc  16805  redc0  16859