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  2206  disjiun  4054  euotd  4317  onsucelsucr  4574  isotr  5908  spc2ed  6342  nninfninc  7251  ltbtwnnqq  7563  genpcdl  7667  genpcuu  7668  un0addcl  9363  un0mulcl  9364  btwnnz  9502  uznfz  10260  elfz0ubfz0  10282  fzoss1  10330  elfzo0z  10345  fzofzim  10349  elfzom1p1elfzo  10380  ssfzo12bi  10391  subfzo0  10408  modfzo0difsn  10577  expaddzap  10765  swrdswrdlem  11195  swrdswrd  11196  swrdccatin1  11216  pfxccatin12lem3  11223  caucvgre  11407  caubnd2  11543  summodc  11809  fzo0dvdseq  12283  nno  12332  lcmdvds  12516  hashgcdeq  12677  modprm0  12692  pcqcl  12744  issubg4m  13644  01eq0ring  14066  neii1  14734  neii2  14736  fsumcncntop  15154  gausslemma2dlem1a  15650