Theorem impancom 447

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

Syntax hints:   -> wi 4   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  eqrdav  2470  rexraleqim  3153  disjiun  4386  euotd  4702  pwssun  4745  isotr  6245  ressuppssdif  6955  oeordi  7306  domunsncan  7690  pssnn  7808  findcard3  7832  ordtypelem7  8057  inf3lem5  8155  r1tr  8265  cardmin2  8450  ac10ct  8483  isf32lem12  8812  isfin1-3  8834  fin17  8842  fin1a2s  8862  axdc4lem  8903  axcclem  8905  ttukeylem2  8958  genpcd  9449  ltexprlem3  9481  prlem936  9490  supsrlem  9553  mul0or  10274  fiminre  10577  un0addcl  10927  un0mulcl  10928  btwnnz  11035  uznfz  11903  elfz0ubfz0  11920  elfzo0z  11985  fzofzim  11990  elfzom1p1elfzo  12022  ssfzoulel  12034  ssfzo12bi  12035  subfzo0  12058  modaddmodup  12187  modfzo0difsn  12195  axdc4uzlem  12233  expaddz  12354  sq01  12432  hashnn0n0nn  12608  hashss  12624  hashgt12el  12636  fi1uzind  12691  brfi1indALT  12694  fi1uzindOLD  12697  brfi1indALTOLD  12700  ccatalpha  12787  swrdswrdlem  12869  swrdswrd  12870  swrdccatin1  12893  swrdccatin12lem3  12900  repswswrd  12941  cshwmodn  12951  cshf1  12966  cshw1  12978  2cshwcshw  12981  sqrmo  13392  caubnd2  13497  summo  13860  divalglem8  14459  lcmdvds  14652  lcmfunsnlem1  14689  modprm0  14835  pcqcl  14885  vdwnnlem3  15026  prmgaplem5  15104  prmgaplem7  15106  catpropd  15692  cicsym  15787  isinitoi  15976  istermoi  15977  iszeroi  15982  acsfiindd  16501  tsrlemax  16544  issubg4  16914  gsmsymgreqlem2  17150  oddvdsnn0  17271  oddvds  17274  gexdvds  17313  lt6abl  17607  pgpfac1lem3  17788  coe1ae0  18886  isphld  19298  mdetdiaglem  19700  slesolex  19784  pmatcoe1fsupp  19802  cpmatelimp  19813  cpmatelimp2  19815  cpmatmcllem  19819  pm2mpf1  19900  mp2pm2mplem4  19910  fvmptnn04ifa  19951  fvmptnn04ifd  19954  chfacfscmul0  19959  chfacfpmmul0  19963  neii1  20199  neii2  20201  uncmp  20495  isfild  20951  fbunfip  20962  fgss2  20967  fgcl  20971  isufil2  21001  cfinufil  21021  ufilen  21023  fsumcn  21980  lmmbr  22306  iscau4  22327  caussi  22345  ovoliunnul  22538  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  itg1ge0a  22748  rolle  23021  ulmcaulem  23428  cxpge0  23707  fsumvma  24220  2sqb  24385  pntrsumbnd2  24484  pntlem3  24526  axeuclid  25072  axcontlem2  25074  nbcusgra  25270  cusgrares  25279  usgrasscusgra  25290  sizeusglecusglem1  25291  usgrwlknloop  25372  wlkdvspthlem  25416  usgra2wlkspthlem2  25427  fargshiftf  25443  wwlknimp  25494  wlkiswwlk2lem5  25502  vfwlkniswwlkn  25513  usg2wlkeq  25515  wlkiswwlksur  25526  clwwlkgt0  25578  clwlkisclwwlklem2a4  25591  clwlkisclwwlklem2a  25592  clwwlkel  25600  wwlksubclwwlk  25611  clwwisshclwwlem1  25612  clwlkfoclwwlk  25652  usg2spthonot0  25696  vdgn1frgrav3  25835  frgrancvvdeqlem3  25839  frgrancvvdeqlem4  25840  extwwlkfablem2  25885  numclwwlkun  25886  numclwwlkovf2ex  25893  frgraregord013  25925  ghgrpOLD  26177  ghabloOLD  26178  spansncvi  27386  lnconi  27767  cdj3lem1  28168  spc2ed  28187  metider  28771  ghomf1olem  30384  nofv  30615  sltres  30622  finminlem  31045  clsint2  31056  bj-finsumval0  31772  finxpsuclem  31859  wl-exeq  31937  phpreu  31993  poimirlem26  32030  poimir  32037  ismtyima  32199  elpaddn0  33436  tendospcanN  34662  rexzrexnn0  35718  unxpwdom3  36024  hashgcdeq  36146  radcnvrat  36733  propeqop  39146  funopsn  39164  zm1nn  39194  subsubelfzo0  39207  fzoopth  39208  2ffzoeq  39209  upgredg  39389  usgrislfuspgr  39432  nbuhgr2vtx1edgblem  39583  usgredgsscusgredg  39685  upgr1wlkvtxedg  39847  uspgrn2crct  39986  crctcsh1wlkn0lem4  39991  uhgr3cyclexlem  40095  usgra2pthspth  40173  isassintop  40354  uzlidlring  40437  2zrngamgm  40447  ply1mulgsumlem1  40686  suppdm  40812  nno  40836