Theorem impancom 256

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 113	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 77	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	imp 122	1 |- ( ( ph /\ ch ) -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  eqrdav  2080  euotd  4009  onsucelsucr  4252  isotr  5476  spc2ed  5874  ltbtwnnqq  6605  genpcdl  6709  genpcuu  6710  un0addcl  8321  un0mulcl  8322  btwnnz  8441  uznfz  9120  elfz0ubfz0  9136  fzoss1  9180  elfzo0z  9193  fzofzim  9197  elfzom1p1elfzo  9223  ssfzo12bi  9234  subfzo0  9251  modfzo0difsn  9397  expaddzap  9520  caucvgre  9867  caubnd2  10003  fzo0dvdseq  10257  nno  10306  lcmdvds  10461