Theorem impancom 438

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  2432  rexraleqim  3074  disjiun  4270  euotd  4580  pwssun  4614  isotr  6014  ressuppssdif  6699  oeordi  7014  domunsncan  7399  pssnn  7519  findcard3  7543  ordtypelem7  7726  inf3lem5  7826  r1tr  7971  cardmin2  8156  ac10ct  8192  isf32lem12  8521  isfin1-3  8543  fin17  8551  fin1a2s  8571  axdc4lem  8612  axcclem  8614  ttukeylem2  8667  genpcd  9163  ltexprlem3  9195  prlem936  9204  supsrlem  9266  mul0or  9964  un0addcl  10601  un0mulcl  10602  btwnnz  10706  elfzelfzelfz  11471  uznfz  11527  elfzo0z  11573  fzofzim  11577  ssfzoulel  11605  ssfzo12bi  11606  modaddmodup  11746  axdc4uzlem  11788  expaddz  11892  sq01  11970  hashnn0n0nn  12137  hashss  12150  hashgt12el  12157  brfi1uzind  12203  swrdswrdlem  12337  swrdswrd  12338  swrdccatin1  12358  swrdccatin12lem3  12365  repswswrd  12406  cshwmodn  12416  cshw1  12440  sqrmo  12725  caubnd2  12829  summo  13178  divalglem8  13587  modprm0  13856  pcqcl  13906  vdwnnlem3  14041  catpropd  14631  acsfiindd  15330  tsrlemax  15373  issubg4  15680  gsmsymgreqlem2  15916  oddvdsnn0  16027  oddvds  16030  gexdvds  16063  lt6abl  16351  pgpfac1lem3  16552  isphld  17925  slesolex  18330  neii1  18552  neii2  18554  uncmp  18848  isfild  19273  fbunfip  19284  fgss2  19289  fgcl  19293  isufil2  19323  cfinufil  19343  ufilen  19345  fsumcn  20288  lmmbr  20611  iscau4  20632  caussi  20650  ovoliunnul  20832  ovolicc2lem4  20845  itg1ge0a  21031  rolle  21304  ulmcaulem  21744  cxpge0  22013  fsumvma  22437  2sqb  22602  pntrsumbnd2  22701  pntlem3  22743  axeuclid  23032  axcontlem2  23034  nbcusgra  23194  cusgrares  23203  usgrasscusgra  23214  sizeusglecusglem1  23215  usgrnloop  23285  wlkdvspthlem  23329  fargshiftf  23345  ghgrp  23678  ghablo  23679  spansncvi  24878  lnconi  25260  cdj3lem1  25661  spc2ed  25680  metider  26175  ghomf1olem  27160  nofv  27645  sltres  27652  wl-exeq  28211  finminlem  28357  clsint2  28368  ismtyima  28546  rexzrexnn0  28987  unxpwdom3  29293  hashgcdeq  29411  subsubelfzo0  30056  fzoopth  30059  2ffzoeq  30060  elfzom1p1elfzo  30061  ccats1rev  30106  usg2wlkeq  30135  usgra2pthspth  30141  usgra2wlkspthlem2  30143  wwlknimp  30167  wlkiswwlk2lem5  30175  vfwlkniswwlkn  30186  wlkiswwlksur  30197  usg2spthonot0  30254  clwwlkgt0  30280  clwlkisclwwlklem2a4  30292  clwlkisclwwlklem2a  30293  clwwlkel  30301  wwlksubclwwlk  30312  zm1nn  30314  clwwisshclwwlem1  30315  cshwlemma1  30335  clwlkfoclwwlk  30364  vdgn1frgrav3  30467  frgrancvvdeqlem3  30471  frgrancvvdeqlem4  30472  extwwlkfablem2  30517  numclwwlkun  30518  numclwwlkovf2ex  30525  frgraregord013  30557  mdetdiaglem  30665  snlindsntorlem  30734  bj-finsumval0  32180  elpaddn0  33038  tendospcanN  34262