Theorem impancom 258

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 114	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	imp 123	1 |- ( ( ph /\ ch ) -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  eqrdav  2138  disjiun  3924  euotd  4176  onsucelsucr  4424  isotr  5717  spc2ed  6130  ltbtwnnqq  7223  genpcdl  7327  genpcuu  7328  un0addcl  9010  un0mulcl  9011  btwnnz  9145  uznfz  9883  elfz0ubfz0  9902  fzoss1  9948  elfzo0z  9961  fzofzim  9965  elfzom1p1elfzo  9991  ssfzo12bi  10002  subfzo0  10019  modfzo0difsn  10168  expaddzap  10337  caucvgre  10753  caubnd2  10889  summodc  11152  fzo0dvdseq  11555  nno  11603  lcmdvds  11760  hashgcdeq  11904  neii1  12316  neii2  12318  fsumcncntop  12725