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  5940  spc2ed  6379  nninfninc  7290  ltbtwnnqq  7602  genpcdl  7706  genpcuu  7707  un0addcl  9402  un0mulcl  9403  btwnnz  9541  uznfz  10299  elfz0ubfz0  10321  fzoss1  10369  elfzo0z  10384  fzofzim  10388  elfzom1p1elfzo  10420  ssfzo12bi  10431  subfzo0  10448  modfzo0difsn  10617  expaddzap  10805  swrdswrdlem  11236  swrdswrd  11237  swrdccatin1  11257  pfxccatin12lem3  11264  caucvgre  11492  caubnd2  11628  summodc  11894  fzo0dvdseq  12368  nno  12417  lcmdvds  12601  hashgcdeq  12762  modprm0  12777  pcqcl  12829  issubg4m  13730  01eq0ring  14153  neii1  14821  neii2  14823  fsumcncntop  15241  gausslemma2dlem1a  15737  usgrislfuspgrdom  15988  upgrwlkvtxedg  16075  uspgr2wlkeq  16076