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  4083  euotd  4347  onsucelsucr  4606  isotr  5957  spc2ed  6398  nninfninc  7322  ltbtwnnqq  7635  genpcdl  7739  genpcuu  7740  un0addcl  9435  un0mulcl  9436  btwnnz  9574  uznfz  10338  elfz0ubfz0  10360  fzoss1  10408  elfzo0z  10424  fzofzim  10428  elfzom1p1elfzo  10460  ssfzo12bi  10471  subfzo0  10489  modfzo0difsn  10658  expaddzap  10846  ccatalpha  11194  swrdswrdlem  11289  swrdswrd  11290  swrdccatin1  11310  pfxccatin12lem3  11317  caucvgre  11559  caubnd2  11695  summodc  11962  fzo0dvdseq  12436  nno  12485  lcmdvds  12669  hashgcdeq  12830  modprm0  12845  pcqcl  12897  issubg4m  13798  01eq0ring  14222  neii1  14890  neii2  14892  fsumcncntop  15310  gausslemma2dlem1a  15806  usgrislfuspgrdom  16060  upgrwlkvtxedg  16234  uspgr2wlkeq  16235  clwwlkccatlem  16270  clwwlknonex2lem2  16308