Theorem impancom 258

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  eqrdav  2169  disjiun  3984  euotd  4239  onsucelsucr  4492  isotr  5795  spc2ed  6212  ltbtwnnqq  7377  genpcdl  7481  genpcuu  7482  un0addcl  9168  un0mulcl  9169  btwnnz  9306  uznfz  10059  elfz0ubfz0  10081  fzoss1  10127  elfzo0z  10140  fzofzim  10144  elfzom1p1elfzo  10170  ssfzo12bi  10181  subfzo0  10198  modfzo0difsn  10351  expaddzap  10520  caucvgre  10945  caubnd2  11081  summodc  11346  fzo0dvdseq  11817  nno  11865  lcmdvds  12033  hashgcdeq  12193  modprm0  12208  pcqcl  12260  neii1  12941  neii2  12943  fsumcncntop  13350