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 ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  eqrdav  2195  disjiun  4029  euotd  4288  onsucelsucr  4545  isotr  5866  spc2ed  6300  nninfninc  7198  ltbtwnnqq  7499  genpcdl  7603  genpcuu  7604  un0addcl  9299  un0mulcl  9300  btwnnz  9437  uznfz  10195  elfz0ubfz0  10217  fzoss1  10264  elfzo0z  10277  fzofzim  10281  elfzom1p1elfzo  10307  ssfzo12bi  10318  subfzo0  10335  modfzo0difsn  10504  expaddzap  10692  caucvgre  11163  caubnd2  11299  summodc  11565  fzo0dvdseq  12039  nno  12088  lcmdvds  12272  hashgcdeq  12433  modprm0  12448  pcqcl  12500  issubg4m  13399  01eq0ring  13821  neii1  14467  neii2  14469  fsumcncntop  14887  gausslemma2dlem1a  15383