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  2230  disjiun  4088  euotd  4353  onsucelsucr  4612  isotr  5967  spc2ed  6407  nninfninc  7382  ltbtwnnqq  7695  genpcdl  7799  genpcuu  7800  un0addcl  9494  un0mulcl  9495  btwnnz  9635  uznfz  10400  elfz0ubfz0  10422  fzoss1  10470  elfzo0z  10486  fzofzim  10490  elfzom1p1elfzo  10522  ssfzo12bi  10533  subfzo0  10551  modfzo0difsn  10720  expaddzap  10908  ccatalpha  11256  swrdswrdlem  11351  swrdswrd  11352  swrdccatin1  11372  pfxccatin12lem3  11379  caucvgre  11621  caubnd2  11757  summodc  12024  fzo0dvdseq  12498  nno  12547  lcmdvds  12731  hashgcdeq  12892  modprm0  12907  pcqcl  12959  issubg4m  13860  01eq0ring  14284  neii1  14958  neii2  14960  fsumcncntop  15378  gausslemma2dlem1a  15877  usgrislfuspgrdom  16131  upgrwlkvtxedg  16305  uspgr2wlkeq  16306  clwwlkccatlem  16341  clwwlknonex2lem2  16379