Theorem impancom 260

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 115	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	imp 124	1 |- ( ( ph /\ ch ) -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  eqrdav  2204  disjiun  4040  euotd  4300  onsucelsucr  4557  isotr  5887  spc2ed  6321  nninfninc  7227  ltbtwnnqq  7530  genpcdl  7634  genpcuu  7635  un0addcl  9330  un0mulcl  9331  btwnnz  9469  uznfz  10227  elfz0ubfz0  10249  fzoss1  10297  elfzo0z  10310  fzofzim  10314  elfzom1p1elfzo  10345  ssfzo12bi  10356  subfzo0  10373  modfzo0difsn  10542  expaddzap  10730  caucvgre  11325  caubnd2  11461  summodc  11727  fzo0dvdseq  12201  nno  12250  lcmdvds  12434  hashgcdeq  12595  modprm0  12610  pcqcl  12662  issubg4m  13562  01eq0ring  13984  neii1  14652  neii2  14654  fsumcncntop  15072  gausslemma2dlem1a  15568