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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  eqrdav  2237  disjiun  4125  euotd  4395  onsucelsucr  4655  isotr  6022  spc2ed  6469  nninfninc  7464  ltbtwnnqq  7783  genpcdl  7887  genpcuu  7888  un0addcl  9601  un0mulcl  9602  btwnnz  9745  uznfz  10521  elfz0ubfz0  10543  fzoss1  10591  elfzo0z  10607  fzofzim  10611  elfzom1p1elfzo  10643  ssfzo12bi  10654  subfzo0  10672  modfzo0difsn  10847  expaddzap  11035  ccatalpha  11397  swrdswrdlem  11492  swrdswrd  11493  swrdccatin1  11513  pfxccatin12lem3  11520  caucvgre  11763  caubnd2  11900  summodc  12169  fzo0dvdseq  12643  nno  12692  lcmdvds  12876  hashgcdeq  13041  modprm0  13056  pcqcl  13108  issubg4m  14049  resscntz  14160  01eq0ring  14580  neii1  15339  neii2  15341  fsumcncntop  15759  gausslemma2dlem1a  16343  usgrislfuspgrdom  16597  upgrwlkvtxedg  16771  uspgr2wlkeq  16772  clwwlkccatlem  16807  clwwlknonex2lem2  16845