Theorem impancom 442

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 436	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 81	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	imp 431	1 |- ( ( ph /\ ch ) -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  eqrdav  2450  rexraleqim  3165  disjiun  4393  euotd  4702  pwssun  4740  isotr  6227  ressuppssdif  6936  oeordi  7288  domunsncan  7672  pssnn  7790  findcard3  7814  ordtypelem7  8039  inf3lem5  8137  r1tr  8247  cardmin2  8432  ac10ct  8465  isf32lem12  8794  isfin1-3  8816  fin17  8824  fin1a2s  8844  axdc4lem  8885  axcclem  8887  ttukeylem2  8940  genpcd  9431  ltexprlem3  9463  prlem936  9472  supsrlem  9535  mul0or  10252  fiminre  10555  un0addcl  10903  un0mulcl  10904  btwnnz  11012  uznfz  11877  elfz0ubfz0  11894  elfzo0z  11958  fzofzim  11962  elfzom1p1elfzo  11993  ssfzoulel  12005  ssfzo12bi  12006  modaddmodup  12153  axdc4uzlem  12195  expaddz  12316  sq01  12394  hashnn0n0nn  12570  hashss  12586  hashgt12el  12595  fi1uzind  12650  brfi1indALT  12653  swrdswrdlem  12815  swrdswrd  12816  swrdccatin1  12839  swrdccatin12lem3  12846  repswswrd  12887  cshwmodn  12897  cshw1  12921  2cshwcshw  12924  sqrmo  13315  caubnd2  13420  summo  13783  divalglem8  14380  lcmdvds  14573  lcmfunsnlem1  14610  modprm0  14756  pcqcl  14806  vdwnnlem3  14947  prmgaplem5  15025  prmgaplem7  15027  catpropd  15614  cicsym  15709  isinitoi  15898  istermoi  15899  iszeroi  15904  acsfiindd  16423  tsrlemax  16466  issubg4  16836  gsmsymgreqlem2  17072  oddvdsnn0  17193  oddvds  17196  gexdvds  17235  lt6abl  17529  pgpfac1lem3  17710  coe1ae0  18809  isphld  19221  mdetdiaglem  19623  slesolex  19707  pmatcoe1fsupp  19725  cpmatelimp  19736  cpmatelimp2  19738  cpmatmcllem  19742  pm2mpf1  19823  mp2pm2mplem4  19833  fvmptnn04ifa  19874  fvmptnn04ifd  19877  chfacfscmul0  19882  chfacfpmmul0  19886  neii1  20122  neii2  20124  uncmp  20418  isfild  20873  fbunfip  20884  fgss2  20889  fgcl  20893  isufil2  20923  cfinufil  20943  ufilen  20945  fsumcn  21902  lmmbr  22228  iscau4  22249  caussi  22267  ovoliunnul  22460  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  itg1ge0a  22669  rolle  22942  ulmcaulem  23349  cxpge0  23628  fsumvma  24141  2sqb  24306  pntrsumbnd2  24405  pntlem3  24447  axeuclid  24993  axcontlem2  24995  nbcusgra  25191  cusgrares  25200  usgrasscusgra  25211  sizeusglecusglem1  25212  usgrwlknloop  25293  wlkdvspthlem  25337  usgra2wlkspthlem2  25348  fargshiftf  25364  wwlknimp  25415  wlkiswwlk2lem5  25423  vfwlkniswwlkn  25434  usg2wlkeq  25436  wlkiswwlksur  25447  clwwlkgt0  25499  clwlkisclwwlklem2a4  25512  clwlkisclwwlklem2a  25513  clwwlkel  25521  wwlksubclwwlk  25532  clwwisshclwwlem1  25533  clwlkfoclwwlk  25573  usg2spthonot0  25617  vdgn1frgrav3  25756  frgrancvvdeqlem3  25760  frgrancvvdeqlem4  25761  extwwlkfablem2  25806  numclwwlkun  25807  numclwwlkovf2ex  25814  frgraregord013  25846  ghgrpOLD  26096  ghabloOLD  26097  spansncvi  27305  lnconi  27686  cdj3lem1  28087  spc2ed  28106  metider  28697  ghomf1olem  30312  nofv  30544  sltres  30551  finminlem  30974  clsint2  30985  bj-finsumval0  31702  finxpsuclem  31789  wl-exeq  31867  phpreu  31929  poimirlem26  31966  poimir  31973  ismtyima  32135  elpaddn0  33365  tendospcanN  34591  rexzrexnn0  35647  unxpwdom3  35953  hashgcdeq  36075  radcnvrat  36663  propeqop  38999  funopsn  39018  zm1nn  39049  subsubelfzo0  39062  fzoopth  39063  2ffzoeq  39064  upgredg  39228  usgr2edg  39291  nbuhgr2vtx1edgblem  39419  usgredgsscusgredg  39520  upgr1wlkvtxedg  39655  usgra2pthspth  39718  isassintop  39899  uzlidlring  39982  2zrngamgm  39992  ply1mulgsumlem1  40231  suppdm  40357  nno  40381