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  2228  disjiun  4078  euotd  4341  onsucelsucr  4600  isotr  5946  spc2ed  6385  nninfninc  7301  ltbtwnnqq  7613  genpcdl  7717  genpcuu  7718  un0addcl  9413  un0mulcl  9414  btwnnz  9552  uznfz  10311  elfz0ubfz0  10333  fzoss1  10381  elfzo0z  10396  fzofzim  10400  elfzom1p1elfzo  10432  ssfzo12bi  10443  subfzo0  10460  modfzo0difsn  10629  expaddzap  10817  ccatalpha  11161  swrdswrdlem  11252  swrdswrd  11253  swrdccatin1  11273  pfxccatin12lem3  11280  caucvgre  11508  caubnd2  11644  summodc  11910  fzo0dvdseq  12384  nno  12433  lcmdvds  12617  hashgcdeq  12778  modprm0  12793  pcqcl  12845  issubg4m  13746  01eq0ring  14169  neii1  14837  neii2  14839  fsumcncntop  15257  gausslemma2dlem1a  15753  usgrislfuspgrdom  16004  upgrwlkvtxedg  16110  uspgr2wlkeq  16111  clwwlkccatlem  16143