Theorem impancom 260

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 115	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	imp 124	1 |- ( ( ph /\ ch ) -> ( ps -> th ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  eqrdav  2237  disjiun  4125  euotd  4395  onsucelsucr  4655  isotr  6022  spc2ed  6469  nninfninc  7463  ltbtwnnqq  7782  genpcdl  7886  genpcuu  7887  un0addcl  9596  un0mulcl  9597  btwnnz  9740  uznfz  10510  elfz0ubfz0  10532  fzoss1  10580  elfzo0z  10596  fzofzim  10600  elfzom1p1elfzo  10632  ssfzo12bi  10643  subfzo0  10661  modfzo0difsn  10832  expaddzap  11020  ccatalpha  11381  swrdswrdlem  11476  swrdswrd  11477  swrdccatin1  11497  pfxccatin12lem3  11504  caucvgre  11747  caubnd2  11883  summodc  12150  fzo0dvdseq  12624  nno  12673  lcmdvds  12857  hashgcdeq  13018  modprm0  13033  pcqcl  13085  issubg4m  13996  01eq0ring  14496  neii1  15248  neii2  15250  fsumcncntop  15668  gausslemma2dlem1a  16177  usgrislfuspgrdom  16431  upgrwlkvtxedg  16605  uspgr2wlkeq  16606  clwwlkccatlem  16641  clwwlknonex2lem2  16679