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  4039  euotd  4299  onsucelsucr  4556  isotr  5885  spc2ed  6319  nninfninc  7225  ltbtwnnqq  7528  genpcdl  7632  genpcuu  7633  un0addcl  9328  un0mulcl  9329  btwnnz  9467  uznfz  10225  elfz0ubfz0  10247  fzoss1  10295  elfzo0z  10308  fzofzim  10312  elfzom1p1elfzo  10343  ssfzo12bi  10354  subfzo0  10371  modfzo0difsn  10540  expaddzap  10728  caucvgre  11292  caubnd2  11428  summodc  11694  fzo0dvdseq  12168  nno  12217  lcmdvds  12401  hashgcdeq  12562  modprm0  12577  pcqcl  12629  issubg4m  13529  01eq0ring  13951  neii1  14619  neii2  14621  fsumcncntop  15039  gausslemma2dlem1a  15535