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  2458  eqrdavOLD  2459  rexraleqim  3222  disjiun  4430  euotd  4741  pwssun  4779  isotr  6211  ressuppssdif  6911  oeordi  7226  domunsncan  7607  pssnn  7728  findcard3  7752  ordtypelem7  7938  inf3lem5  8038  r1tr  8183  cardmin2  8368  ac10ct  8404  isf32lem12  8733  isfin1-3  8755  fin17  8763  fin1a2s  8783  axdc4lem  8824  axcclem  8826  ttukeylem2  8879  genpcd  9373  ltexprlem3  9405  prlem936  9414  supsrlem  9477  mul0or  10178  un0addcl  10818  un0mulcl  10819  btwnnz  10926  uznfz  11750  elfz0ubfz0  11765  elfzo0z  11822  fzofzim  11826  elfzom1p1elfzo  11852  ssfzoulel  11863  ssfzo12bi  11864  modaddmodup  12006  axdc4uzlem  12048  expaddz  12165  sq01  12243  hashnn0n0nn  12413  hashss  12426  hashgt12el  12433  brfi1uzind  12485  swrdswrdlem  12634  swrdswrd  12635  swrdccatin1  12658  swrdccatin12lem3  12665  repswswrd  12706  cshwmodn  12716  cshw1  12740  2cshwcshw  12743  sqrmo  13035  caubnd2  13139  summo  13488  divalglem8  13906  modprm0  14178  pcqcl  14228  vdwnnlem3  14363  catpropd  14954  acsfiindd  15653  tsrlemax  15696  issubg4  16008  gsmsymgreqlem2  16244  oddvdsnn0  16357  oddvds  16360  gexdvds  16393  lt6abl  16681  pgpfac1lem3  16911  coe1ae0  18021  isphld  18449  scmatscm  18775  mdetdiaglem  18860  slesolex  18944  pmatcoe1fsupp  18962  cpmatelimp  18973  cpmatelimp2  18975  cpmatmcllem  18979  pm2mpf1  19060  mp2pm2mplem4  19070  fvmptnn04ifa  19111  fvmptnn04ifd  19114  chfacfscmul0  19119  chfacfpmmul0  19123  neii1  19366  neii2  19368  uncmp  19662  isfild  20087  fbunfip  20098  fgss2  20103  fgcl  20107  isufil2  20137  cfinufil  20157  ufilen  20159  fsumcn  21102  lmmbr  21425  iscau4  21446  caussi  21464  ovoliunnul  21646  ovolicc2lem4  21659  itg1ge0a  21846  rolle  22119  ulmcaulem  22516  cxpge0  22785  fsumvma  23209  2sqb  23374  pntrsumbnd2  23473  pntlem3  23515  axeuclid  23935  axcontlem2  23937  nbcusgra  24125  cusgrares  24134  usgrasscusgra  24145  sizeusglecusglem1  24146  usgrnloop  24227  wlkdvspthlem  24271  usgra2wlkspthlem2  24282  fargshiftf  24298  wwlknimp  24349  wlkiswwlk2lem5  24357  vfwlkniswwlkn  24368  usg2wlkeq  24370  wlkiswwlksur  24381  clwwlkgt0  24433  clwlkisclwwlklem2a4  24446  clwlkisclwwlklem2a  24447  clwwlkel  24455  wwlksubclwwlk  24466  clwwisshclwwlem1  24467  clwlkfoclwwlk  24507  usg2spthonot0  24551  vdgn1frgrav3  24691  frgrancvvdeqlem3  24695  frgrancvvdeqlem4  24696  extwwlkfablem2  24741  numclwwlkun  24742  numclwwlkovf2ex  24749  frgraregord013  24781  ghgrp  25032  ghablo  25033  spansncvi  26232  lnconi  26614  cdj3lem1  27015  spc2ed  27034  metider  27495  ghomf1olem  28495  nofv  28980  sltres  28987  wl-exeq  29550  finminlem  29700  clsint2  29711  ismtyima  29889  rexzrexnn0  30328  unxpwdom3  30634  hashgcdeq  30752  zm1nn  31749  subsubelfzo0  31762  fzoopth  31764  2ffzoeq  31765  usgra2pthspth  31775  ply1mulgsumlem1  31934  snlindsntorlem  32019  bj-finsumval0  33610  elpaddn0  34471  tendospcanN  35695