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  2156  disjiun  3962  euotd  4216  onsucelsucr  4469  isotr  5768  spc2ed  6182  ltbtwnnqq  7337  genpcdl  7441  genpcuu  7442  un0addcl  9128  un0mulcl  9129  btwnnz  9263  uznfz  10011  elfz0ubfz0  10033  fzoss1  10079  elfzo0z  10092  fzofzim  10096  elfzom1p1elfzo  10122  ssfzo12bi  10133  subfzo0  10150  modfzo0difsn  10303  expaddzap  10472  caucvgre  10892  caubnd2  11028  summodc  11291  fzo0dvdseq  11761  nno  11809  lcmdvds  11971  hashgcdeq  12129  modprm0  12144  neii1  12617  neii2  12619  fsumcncntop  13026