Theorem impancom 456

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 450	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 86	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	imp 445	1 |- ( ( ph /\ ch ) -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  eqrdav  2621  rexraleqim  3328  disjiun  4640  disjord  4641  disjiund  4643  propeqop  4970  euotd  4975  pwssun  5020  funopsn  6413  isotr  6586  el2mpt2csbcl  7250  ressuppssdif  7316  oeordi  7667  domunsncan  8060  pssnn  8178  findcard3  8203  ordtypelem7  8429  inf3lem5  8529  r1tr  8639  cardmin2  8824  ac10ct  8857  isf32lem12  9186  isfin1-3  9208  fin17  9216  fin1a2s  9236  axdc4lem  9277  axcclem  9279  ttukeylem2  9332  genpcd  9828  ltexprlem3  9860  prlem936  9869  supsrlem  9932  mul0or  10667  fiminre  10972  un0addcl  11326  un0mulcl  11327  btwnnz  11453  uznfz  12423  elfz0ubfz0  12443  elfzo0z  12509  fzofzim  12514  elfzom1p1elfzo  12547  ssfzoulel  12562  ssfzo12bi  12563  subfzo0  12590  modmuladdim  12713  modaddmodup  12733  modfzo0difsn  12742  axdc4uzlem  12782  expaddz  12904  sq01  12986  hashnn0n0nn  13180  hashss  13197  hashgt12el  13210  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  ccatalpha  13375  swrdswrdlem  13459  swrdswrd  13460  swrdccatin1  13483  swrdccatin12lem3  13490  repswswrd  13531  cshwmodn  13541  cshf1  13556  cshw1  13568  2cshwcshw  13571  sqrmo  13992  caubnd2  14097  summo  14448  nno  15098  divalglem8  15123  lcmdvds  15321  lcmfunsnlem1  15350  hashgcdeq  15494  modprm0  15510  pcqcl  15561  vdwnnlem3  15701  prmgaplem5  15759  prmgaplem7  15761  catpropd  16369  cicsym  16464  isinitoi  16653  istermoi  16654  iszeroi  16659  acsfiindd  17177  tsrlemax  17220  issubg4  17613  gsmsymgreqlem2  17851  oddvdsnn0  17963  oddvds  17966  gexdvds  17999  lt6abl  18296  pgpfac1lem3  18476  coe1ae0  19586  isphld  19999  mdetdiaglem  20404  slesolex  20488  pmatcoe1fsupp  20506  cpmatelimp  20517  cpmatelimp2  20519  cpmatmcllem  20523  pm2mpf1  20604  mp2pm2mplem4  20614  fvmptnn04ifa  20655  fvmptnn04ifd  20658  chfacfscmul0  20663  chfacfpmmul0  20667  neii1  20910  neii2  20912  uncmp  21206  isfild  21662  fbunfip  21673  fgss2  21678  fgcl  21682  isufil2  21712  cfinufil  21732  ufilen  21734  fsumcn  22673  lmmbr  23056  iscau4  23077  caussi  23095  ovoliunnul  23275  ovolicc2lem4  23288  itg1ge0a  23478  rolle  23753  ulmcaulem  24148  cxpge0  24429  fsumvma  24938  gausslemma2dlem1a  25090  2sqb  25157  pntrsumbnd2  25256  pntlem3  25298  axeuclid  25843  axcontlem2  25845  usgrislfuspgr  26079  nbuhgr2vtx1edgblem  26247  usgredgsscusgredg  26355  upgrwlkvtxedg  26541  uspgr2wlkeq  26542  cyclnspth  26695  uspgrn2crct  26700  crctcshwlkn0lem4  26705  wlkiswwlks2lem5  26759  wlknewwlksn  26773  wlkwwlksur  26783  umgrwwlks2on  26850  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwwlksel  26914  wwlksubclwwlks  26925  clwwisshclwwslemlem  26926  clwlksfoclwwlk  26963  uhgr3cyclexlem  27041  vdgn1frgrv3  27161  2wspmdisj  27201  numclwwlkovf2exlem2  27212  frgrregord013  27253  spansncvi  28511  lnconi  28892  cdj3lem1  29293  spc2ed  29312  metider  29937  funeldmb  31661  nofv  31810  sltres  31815  finminlem  32312  clsint2  32324  bj-finsumval0  33147  finxpsuclem  33234  wl-exeq  33321  phpreu  33393  poimirlem26  33435  poimir  33442  ismtyima  33602  elpaddn0  35086  tendospcanN  36312  rexzrexnn0  37368  unxpwdom3  37665  fsovrfovd  38303  radcnvrat  38513  zm1nn  41316  subsubelfzo0  41336  fzoopth  41337  2ffzoeq  41338  fargshiftf  41376  2pwp1prm  41503  lighneal  41528  isassintop  41846  uzlidlring  41929  2zrngamgm  41939  ply1mulgsumlem1  42174  suppdm  42300