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  4025  euotd  4284  onsucelsucr  4541  isotr  5860  spc2ed  6288  nninfninc  7184  ltbtwnnqq  7477  genpcdl  7581  genpcuu  7582  un0addcl  9276  un0mulcl  9277  btwnnz  9414  uznfz  10172  elfz0ubfz0  10194  fzoss1  10241  elfzo0z  10254  fzofzim  10258  elfzom1p1elfzo  10284  ssfzo12bi  10295  subfzo0  10312  modfzo0difsn  10469  expaddzap  10657  caucvgre  11128  caubnd2  11264  summodc  11529  fzo0dvdseq  12002  nno  12050  lcmdvds  12220  hashgcdeq  12380  modprm0  12395  pcqcl  12447  issubg4m  13266  01eq0ring  13688  neii1  14326  neii2  14328  fsumcncntop  14746  gausslemma2dlem1a  15215