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  3999  euotd  4255  onsucelsucr  4508  isotr  5817  spc2ed  6234  ltbtwnnqq  7414  genpcdl  7518  genpcuu  7519  un0addcl  9209  un0mulcl  9210  btwnnz  9347  uznfz  10103  elfz0ubfz0  10125  fzoss1  10171  elfzo0z  10184  fzofzim  10188  elfzom1p1elfzo  10214  ssfzo12bi  10225  subfzo0  10242  modfzo0difsn  10395  expaddzap  10564  caucvgre  10990  caubnd2  11126  summodc  11391  fzo0dvdseq  11863  nno  11911  lcmdvds  12079  hashgcdeq  12239  modprm0  12254  pcqcl  12306  issubg4m  13053  01eq0ring  13330  neii1  13650  neii2  13652  fsumcncntop  14059