Theorem impancom 440

Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)

Hypothesis

Ref	Expression
impancom.1	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Assertion

Ref	Expression
impancom	|- ( ( ph /\ ch ) -> ( ps -> th ) )

Proof of Theorem impancom

Step	Hyp	Ref	Expression
1		impancom.1	. . . 4 |- ( ( ph /\ ps ) -> ( ch -> th ) )
2	1	ex 434	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	imp 429	1 |- ( ( ph /\ ch ) -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  eqrdav  2442  rexraleqim  3088  disjiun  4285  euotd  4595  pwssun  4630  isotr  6030  ressuppssdif  6713  oeordi  7029  domunsncan  7414  pssnn  7534  findcard3  7558  ordtypelem7  7741  inf3lem5  7841  r1tr  7986  cardmin2  8171  ac10ct  8207  isf32lem12  8536  isfin1-3  8558  fin17  8566  fin1a2s  8586  axdc4lem  8627  axcclem  8629  ttukeylem2  8682  genpcd  9178  ltexprlem3  9210  prlem936  9219  supsrlem  9281  mul0or  9979  un0addcl  10616  un0mulcl  10617  btwnnz  10721  elfzelfzelfz  11487  uznfz  11546  elfzo0z  11592  fzofzim  11596  ssfzoulel  11624  ssfzo12bi  11625  modaddmodup  11765  axdc4uzlem  11807  expaddz  11911  sq01  11989  hashnn0n0nn  12156  hashss  12169  hashgt12el  12176  brfi1uzind  12222  swrdswrdlem  12356  swrdswrd  12357  swrdccatin1  12377  swrdccatin12lem3  12384  repswswrd  12425  cshwmodn  12435  cshw1  12459  sqrmo  12744  caubnd2  12848  summo  13197  divalglem8  13607  modprm0  13876  pcqcl  13926  vdwnnlem3  14061  catpropd  14651  acsfiindd  15350  tsrlemax  15393  issubg4  15703  gsmsymgreqlem2  15939  oddvdsnn0  16050  oddvds  16053  gexdvds  16086  lt6abl  16374  pgpfac1lem3  16581  isphld  18086  slesolex  18491  neii1  18713  neii2  18715  uncmp  19009  isfild  19434  fbunfip  19445  fgss2  19450  fgcl  19454  isufil2  19484  cfinufil  19504  ufilen  19506  fsumcn  20449  lmmbr  20772  iscau4  20793  caussi  20811  ovoliunnul  20993  ovolicc2lem4  21006  itg1ge0a  21192  rolle  21465  ulmcaulem  21862  cxpge0  22131  fsumvma  22555  2sqb  22720  pntrsumbnd2  22819  pntlem3  22861  axeuclid  23212  axcontlem2  23214  nbcusgra  23374  cusgrares  23383  usgrasscusgra  23394  sizeusglecusglem1  23395  usgrnloop  23465  wlkdvspthlem  23509  fargshiftf  23525  ghgrp  23858  ghablo  23859  spansncvi  25058  lnconi  25440  cdj3lem1  25841  spc2ed  25860  metider  26324  ghomf1olem  27316  nofv  27801  sltres  27808  wl-exeq  28366  finminlem  28516  clsint2  28527  ismtyima  28705  rexzrexnn0  29145  unxpwdom3  29451  hashgcdeq  29569  subsubelfzo0  30213  fzoopth  30216  2ffzoeq  30217  elfzom1p1elfzo  30218  ccats1rev  30263  usg2wlkeq  30292  usgra2pthspth  30298  usgra2wlkspthlem2  30300  wwlknimp  30324  wlkiswwlk2lem5  30332  vfwlkniswwlkn  30343  wlkiswwlksur  30354  usg2spthonot0  30411  clwwlkgt0  30437  clwlkisclwwlklem2a4  30449  clwlkisclwwlklem2a  30450  clwwlkel  30458  wwlksubclwwlk  30469  zm1nn  30471  clwwisshclwwlem1  30472  cshwlemma1  30492  clwlkfoclwwlk  30521  vdgn1frgrav3  30624  frgrancvvdeqlem3  30628  frgrancvvdeqlem4  30629  extwwlkfablem2  30674  numclwwlkun  30675  numclwwlkovf2ex  30682  frgraregord013  30714  coe1ae0  30835  ply1mulgsumlem1  30847  scmatsubcl  30887  scmatmulcl  30889  pmatcoe1fsupp  30895  mp2pm2mplem4  30922  mdetdiaglem  30938  snlindsntorlem  31007  bj-finsumval0  32586  elpaddn0  33447  tendospcanN  34671