Theorem impcom 124

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 123	1 |- ( ( ps /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  mpan9  279  19.41h  1664  19.41  1665  equtr2  1688  mopick  2078  2euex  2087  gencl  2721  2gencl  2722  rspccva  2792  indifdir  3337  sseq0  3409  minel  3429  r19.2m  3454  r19.2mOLD  3455  elelpwi  3527  ssuni  3766  disjiun  3932  trintssm  4050  ssexg  4075  pofun  4242  sowlin  4250  2optocl  4624  3optocl  4625  elrnmpt1  4798  resieq  4837  fnun  5237  fss  5292  fun  5303  dmfex  5320  fvelimab  5485  mptfvex  5514  fmptco  5594  fnressn  5614  fressnfv  5615  fvtp2g  5637  fvtp3g  5638  fnex  5650  funfvima3  5659  isores3  5724  f1o2ndf1  6133  reldmtpos  6158  smores  6197  tfrlem7  6222  tfrlemi1  6237  tfrexlem  6239  tfrcl  6269  frecrdg  6313  nnacl  6384  nnmcl  6385  nnmsucr  6392  nntri3or  6397  nnaword  6415  nnaordex  6431  2ecoptocl  6525  ssct  6720  enm  6722  xpf1o  6746  ac6sfi  6800  f1dmvrnfibi  6840  f1vrnfibi  6841  updjud  6975  enumct  7008  elni2  7146  ax1rid  7709  negf1o  8168  mulgt1  8645  lbreu  8727  nnaddcl  8764  nnmulcl  8765  zaddcllempos  9115  zaddcllemneg  9117  nn0n0n1ge2b  9154  fzind  9190  fnn0ind  9191  uzaddcl  9408  elpq  9467  uzsubsubfz  9858  elfz1b  9901  elfz0ubfz0  9933  fz0fzdiffz0  9938  elfzmlbp  9940  fzofzim  9996  elfzom1elp1fzo  10010  elfzom1p1elfzo  10022  ssfzo12bi  10033  modfzo0difsn  10199  seq3val  10262  seqvalcd  10263  expcllem  10335  expap0  10354  apexp1  10496  faclbnd  10519  faclbnd6  10522  fihashf1rn  10567  omgadd  10580  hashfzp1  10602  seq3coll  10617  cjexp  10697  r19.29uz  10796  resqrexlemover  10814  resqrexlemlo  10817  resqrexlemcalc3  10820  absexp  10883  fimaxre2  11030  climshft  11105  climub  11145  climserle  11146  sumfct  11175  isumss2  11194  binom  11285  bcxmas  11290  clim2prod  11340  prodfap0  11346  prodfrecap  11347  demoivreALT  11516  dvdsdivcl  11584  dvdsfac  11594  oddnn02np1  11613  oddge22np1  11614  evennn02n  11615  evennn2n  11616  m1exp1  11634  nn0o  11640  flodddiv4  11667  gcdneg  11706  bezoutlemmain  11722  dfgcd2  11738  gcdmultiple  11744  alginv  11764  cncongr1  11820  prmdvdsexp  11862  prmndvdsfaclt  11870  clsss  12326  xmettri2  12569  mettri  12581  metss  12702  bdssexg  13273  bj-findis  13348  nninfalllemn  13377  nninfalllem1  13378  nninfsellemdc  13381