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  2176  disjiun  3997  euotd  4253  onsucelsucr  4506  isotr  5813  spc2ed  6230  ltbtwnnqq  7410  genpcdl  7514  genpcuu  7515  un0addcl  9204  un0mulcl  9205  btwnnz  9342  uznfz  10097  elfz0ubfz0  10119  fzoss1  10165  elfzo0z  10178  fzofzim  10182  elfzom1p1elfzo  10208  ssfzo12bi  10219  subfzo0  10236  modfzo0difsn  10389  expaddzap  10558  caucvgre  10982  caubnd2  11118  summodc  11383  fzo0dvdseq  11854  nno  11902  lcmdvds  12070  hashgcdeq  12230  modprm0  12245  pcqcl  12297  issubg4m  12983  01eq0ring  13252  neii1  13509  neii2  13511  fsumcncntop  13918