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  2139  disjiun  3932  euotd  4184  onsucelsucr  4432  isotr  5725  spc2ed  6138  ltbtwnnqq  7247  genpcdl  7351  genpcuu  7352  un0addcl  9034  un0mulcl  9035  btwnnz  9169  uznfz  9914  elfz0ubfz0  9933  fzoss1  9979  elfzo0z  9992  fzofzim  9996  elfzom1p1elfzo  10022  ssfzo12bi  10033  subfzo0  10050  modfzo0difsn  10199  expaddzap  10368  caucvgre  10785  caubnd2  10921  summodc  11184  fzo0dvdseq  11591  nno  11639  lcmdvds  11796  hashgcdeq  11940  neii1  12355  neii2  12357  fsumcncntop  12764