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  2441  eqrdavOLD  2442  rexraleqim  3211  disjiun  4427  euotd  4738  pwssun  4776  isotr  6217  ressuppssdif  6923  oeordi  7238  domunsncan  7619  pssnn  7740  findcard3  7765  ordtypelem7  7952  inf3lem5  8052  r1tr  8197  cardmin2  8382  ac10ct  8418  isf32lem12  8747  isfin1-3  8769  fin17  8777  fin1a2s  8797  axdc4lem  8838  axcclem  8840  ttukeylem2  8893  genpcd  9387  ltexprlem3  9419  prlem936  9428  supsrlem  9491  mul0or  10195  un0addcl  10835  un0mulcl  10836  btwnnz  10945  uznfz  11770  elfz0ubfz0  11786  elfzo0z  11844  fzofzim  11848  elfzom1p1elfzo  11874  ssfzoulel  11885  ssfzo12bi  11886  modaddmodup  12029  axdc4uzlem  12071  expaddz  12189  sq01  12267  hashnn0n0nn  12437  hashss  12453  hashgt12el  12460  brfi1uzind  12511  swrdswrdlem  12663  swrdswrd  12664  swrdccatin1  12687  swrdccatin12lem3  12694  repswswrd  12735  cshwmodn  12745  cshw1  12769  2cshwcshw  12772  sqrmo  13064  caubnd2  13169  summo  13518  divalglem8  13935  modprm0  14207  pcqcl  14257  vdwnnlem3  14392  catpropd  14981  acsfiindd  15681  tsrlemax  15724  issubg4  16094  gsmsymgreqlem2  16330  oddvdsnn0  16442  oddvds  16445  gexdvds  16478  lt6abl  16771  pgpfac1lem3  17002  coe1ae0  18131  isphld  18562  mdetdiaglem  18973  slesolex  19057  pmatcoe1fsupp  19075  cpmatelimp  19086  cpmatelimp2  19088  cpmatmcllem  19092  pm2mpf1  19173  mp2pm2mplem4  19183  fvmptnn04ifa  19224  fvmptnn04ifd  19227  chfacfscmul0  19232  chfacfpmmul0  19236  neii1  19480  neii2  19482  uncmp  19776  isfild  20232  fbunfip  20243  fgss2  20248  fgcl  20252  isufil2  20282  cfinufil  20302  ufilen  20304  fsumcn  21247  lmmbr  21570  iscau4  21591  caussi  21609  ovoliunnul  21791  ovolicc2lem4  21804  itg1ge0a  21991  rolle  22264  ulmcaulem  22661  cxpge0  22936  fsumvma  23360  2sqb  23525  pntrsumbnd2  23624  pntlem3  23666  axeuclid  24138  axcontlem2  24140  nbcusgra  24335  cusgrares  24344  usgrasscusgra  24355  sizeusglecusglem1  24356  usgrnloop  24437  wlkdvspthlem  24481  usgra2wlkspthlem2  24492  fargshiftf  24508  wwlknimp  24559  wlkiswwlk2lem5  24567  vfwlkniswwlkn  24578  usg2wlkeq  24580  wlkiswwlksur  24591  clwwlkgt0  24643  clwlkisclwwlklem2a4  24656  clwlkisclwwlklem2a  24657  clwwlkel  24665  wwlksubclwwlk  24676  clwwisshclwwlem1  24677  clwlkfoclwwlk  24717  usg2spthonot0  24761  vdgn1frgrav3  24900  frgrancvvdeqlem3  24904  frgrancvvdeqlem4  24905  extwwlkfablem2  24950  numclwwlkun  24951  numclwwlkovf2ex  24958  frgraregord013  24990  ghgrpOLD  25242  ghabloOLD  25243  spansncvi  26442  lnconi  26824  cdj3lem1  27225  spc2ed  27244  metider  27746  ghomf1olem  28907  nofv  29392  sltres  29399  wl-exeq  29962  finminlem  30111  clsint2  30122  ismtyima  30274  rexzrexnn0  30712  unxpwdom3  31016  hashgcdeq  31134  radcnvrat  31171  lcmdvds  31190  zm1nn  32163  subsubelfzo0  32176  fzoopth  32178  2ffzoeq  32179  usgra2pthspth  32189  isassintop  32371  uzlidlring  32445  2zrngamgm  32455  ply1mulgsumlem1  32721  bj-finsumval0  34403  elpaddn0  35264  tendospcanN  36490