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  2176  disjiun  3998  euotd  4254  onsucelsucr  4507  isotr  5816  spc2ed  6233  ltbtwnnqq  7413  genpcdl  7517  genpcuu  7518  un0addcl  9208  un0mulcl  9209  btwnnz  9346  uznfz  10102  elfz0ubfz0  10124  fzoss1  10170  elfzo0z  10183  fzofzim  10187  elfzom1p1elfzo  10213  ssfzo12bi  10224  subfzo0  10241  modfzo0difsn  10394  expaddzap  10563  caucvgre  10989  caubnd2  11125  summodc  11390  fzo0dvdseq  11862  nno  11910  lcmdvds  12078  hashgcdeq  12238  modprm0  12253  pcqcl  12305  issubg4m  13051  01eq0ring  13328  neii1  13617  neii2  13619  fsumcncntop  14026