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  2087  disjiun  3840  euotd  4081  onsucelsucr  4325  isotr  5595  spc2ed  5998  ltbtwnnqq  6972  genpcdl  7076  genpcuu  7077  un0addcl  8704  un0mulcl  8705  btwnnz  8838  uznfz  9513  elfz0ubfz0  9532  fzoss1  9578  elfzo0z  9591  fzofzim  9595  elfzom1p1elfzo  9621  ssfzo12bi  9632  subfzo0  9649  modfzo0difsn  9798  expaddzap  9995  caucvgre  10410  caubnd2  10546  isummo  10769  fzo0dvdseq  11132  nno  11180  lcmdvds  11335  hashgcdeq  11478