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  2192  disjiun  4024  euotd  4283  onsucelsucr  4540  isotr  5859  spc2ed  6286  nninfninc  7182  ltbtwnnqq  7475  genpcdl  7579  genpcuu  7580  un0addcl  9273  un0mulcl  9274  btwnnz  9411  uznfz  10169  elfz0ubfz0  10191  fzoss1  10238  elfzo0z  10251  fzofzim  10255  elfzom1p1elfzo  10281  ssfzo12bi  10292  subfzo0  10309  modfzo0difsn  10466  expaddzap  10654  caucvgre  11125  caubnd2  11261  summodc  11526  fzo0dvdseq  11999  nno  12047  lcmdvds  12217  hashgcdeq  12377  modprm0  12392  pcqcl  12444  issubg4m  13263  01eq0ring  13685  neii1  14315  neii2  14317  fsumcncntop  14724  gausslemma2dlem1a  15174