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  2164  disjiun  3976  euotd  4231  onsucelsucr  4484  isotr  5783  spc2ed  6197  ltbtwnnqq  7352  genpcdl  7456  genpcuu  7457  un0addcl  9143  un0mulcl  9144  btwnnz  9281  uznfz  10034  elfz0ubfz0  10056  fzoss1  10102  elfzo0z  10115  fzofzim  10119  elfzom1p1elfzo  10145  ssfzo12bi  10156  subfzo0  10173  modfzo0difsn  10326  expaddzap  10495  caucvgre  10919  caubnd2  11055  summodc  11320  fzo0dvdseq  11791  nno  11839  lcmdvds  12007  hashgcdeq  12167  modprm0  12182  pcqcl  12234  neii1  12747  neii2  12749  fsumcncntop  13156