Theorem impancom 441

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  eqrdav  2420  eqrdavOLD  2421  rexraleqim  3197  disjiun  4411  euotd  4718  pwssun  4756  isotr  6239  ressuppssdif  6944  oeordi  7293  domunsncan  7675  pssnn  7793  findcard3  7817  ordtypelem7  8042  inf3lem5  8140  r1tr  8249  cardmin2  8434  ac10ct  8466  isf32lem12  8795  isfin1-3  8817  fin17  8825  fin1a2s  8845  axdc4lem  8886  axcclem  8888  ttukeylem2  8941  genpcd  9432  ltexprlem3  9464  prlem936  9473  supsrlem  9536  mul0or  10253  fiminre  10556  un0addcl  10904  un0mulcl  10905  btwnnz  11013  uznfz  11878  elfz0ubfz0  11895  elfzo0z  11959  fzofzim  11963  elfzom1p1elfzo  11993  ssfzoulel  12005  ssfzo12bi  12006  modaddmodup  12153  axdc4uzlem  12195  expaddz  12316  sq01  12394  hashnn0n0nn  12570  hashss  12586  hashgt12el  12593  brfi1uzind  12647  swrdswrdlem  12806  swrdswrd  12807  swrdccatin1  12830  swrdccatin12lem3  12837  repswswrd  12878  cshwmodn  12888  cshw1  12912  2cshwcshw  12915  sqrmo  13304  caubnd2  13409  summo  13771  divalglem8  14368  lcmdvds  14561  lcmfunsnlem1  14598  modprm0  14744  pcqcl  14794  vdwnnlem3  14935  prmgaplem5  15013  prmgaplem7  15015  catpropd  15602  cicsym  15697  isinitoi  15886  istermoi  15887  iszeroi  15892  acsfiindd  16411  tsrlemax  16454  issubg4  16824  gsmsymgreqlem2  17060  oddvdsnn0  17181  oddvds  17184  gexdvds  17223  lt6abl  17517  pgpfac1lem3  17698  coe1ae0  18797  isphld  19208  mdetdiaglem  19610  slesolex  19694  pmatcoe1fsupp  19712  cpmatelimp  19723  cpmatelimp2  19725  cpmatmcllem  19729  pm2mpf1  19810  mp2pm2mplem4  19820  fvmptnn04ifa  19861  fvmptnn04ifd  19864  chfacfscmul0  19869  chfacfpmmul0  19873  neii1  20109  neii2  20111  uncmp  20405  isfild  20860  fbunfip  20871  fgss2  20876  fgcl  20880  isufil2  20910  cfinufil  20930  ufilen  20932  fsumcn  21889  lmmbr  22215  iscau4  22236  caussi  22254  ovoliunnul  22447  ovolicc2lem4OLD  22460  ovolicc2lem4  22461  itg1ge0a  22656  rolle  22929  ulmcaulem  23336  cxpge0  23615  fsumvma  24128  2sqb  24293  pntrsumbnd2  24392  pntlem3  24434  axeuclid  24980  axcontlem2  24982  nbcusgra  25177  cusgrares  25186  usgrasscusgra  25197  sizeusglecusglem1  25198  usgrwlknloop  25279  wlkdvspthlem  25323  usgra2wlkspthlem2  25334  fargshiftf  25350  wwlknimp  25401  wlkiswwlk2lem5  25409  vfwlkniswwlkn  25420  usg2wlkeq  25422  wlkiswwlksur  25433  clwwlkgt0  25485  clwlkisclwwlklem2a4  25498  clwlkisclwwlklem2a  25499  clwwlkel  25507  wwlksubclwwlk  25518  clwwisshclwwlem1  25519  clwlkfoclwwlk  25559  usg2spthonot0  25603  vdgn1frgrav3  25742  frgrancvvdeqlem3  25746  frgrancvvdeqlem4  25747  extwwlkfablem2  25792  numclwwlkun  25793  numclwwlkovf2ex  25800  frgraregord013  25832  ghgrpOLD  26082  ghabloOLD  26083  spansncvi  27291  lnconi  27672  cdj3lem1  28073  spc2ed  28092  metider  28693  ghomf1olem  30308  nofv  30539  sltres  30546  finminlem  30967  clsint2  30978  bj-finsumval0  31654  wl-exeq  31781  phpreu  31843  poimirlem26  31880  poimir  31887  ismtyima  32049  elpaddn0  33284  tendospcanN  34510  rexzrexnn0  35566  unxpwdom3  35873  hashgcdeq  35995  radcnvrat  36521  propeqop  38704  funopsn  38717  zm1nn  38738  subsubelfzo0  38751  fzoopth  38752  2ffzoeq  38753  usgr2edg  38914  usgra2pthspth  38937  isassintop  39118  uzlidlring  39201  2zrngamgm  39211  ply1mulgsumlem1  39452  suppdm  39578  nno  39602